Theorem syl5bir 233

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
syl5bir.1	|- ( ps <-> ph )
syl5bir.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5bir	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5bir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 |- ( ps <-> ph )
2	1	biimpri 218	. 2 |- ( ph -> ps )
3		syl5bir.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 34	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  3imtr3g  284  oplem1  1007  nic-ax  1598  19.30  1809  19.33b  1813  hbntOLD  2145  necon1bd  2812  pssdifn0  3944  ssdisjOLD  4027  ralnralall  4080  disjss3  4652  somo  5069  frminex  5094  sofld  5581  ordelord  5745  unizlim  5844  f0rn0  6090  funopfv  6235  mpteqb  6299  fvrnressn  6428  funfvima  6492  fpropnf1  6524  fliftfun  6562  weniso  6604  tfinds  7059  tfindsg  7060  tfindes  7062  tfinds2  7063  findsg  7093  frxp  7287  suppssr  7326  rdgsucmptnf  7525  frsucmptn  7534  tz7.49  7540  om00  7655  oewordi  7671  iiner  7819  eroveu  7842  undom  8048  sdomdif  8108  php3  8146  sucdom2  8156  unxpdomlem3  8166  fisseneq  8171  pssnn  8178  ordunifi  8210  isfinite2  8218  fiint  8237  infssuni  8257  ixpfi2  8264  finsschain  8273  ordtypelem10  8432  wofib  8450  wemapsolem  8455  unxpwdom2  8493  inf3lem2  8526  cantnfp1lem3  8577  cantnfp1  8578  setind  8610  r1tr  8639  r1ordg  8641  rankelb  8687  rankxplim3  8744  cardlim  8798  infxpenlem  8836  infxpenc2  8845  dfac5lem4  8949  dfac12k  8969  kmlem13  8984  sornom  9099  fin23lem25  9146  fin23lem21  9161  zorn2lem4  9321  iundom2g  9362  fpwwe2lem12  9463  fpwwe2lem13  9464  pwfseqlem4a  9483  eltsk2g  9573  inttsk  9596  tskord  9602  r1tskina  9604  grudomon  9639  arch  11289  zaddcl  11417  uzm1  11718  xrsupsslem  12137  xrinfmsslem  12138  fsequb  12774  fseqsupubi  12777  ssnn0fi  12784  seqf1o  12842  sq01  12986  ccatalpha  13375  swrdccatin1  13483  repsdf2  13525  cshw1  13568  wrdl3s3  13705  rexanre  14086  rexuzre  14092  cau3lem  14094  o1co  14317  rlimcn2  14321  o1of2  14343  lo1add  14357  lo1mul  14358  climcau  14401  climbdd  14402  caucvgb  14410  summo  14448  isumltss  14580  mertenslem2  14617  prodmolem2  14665  prodmo  14666  dvdsaddre2b  15029  bitsfzolem  15156  bitsfzo  15157  bezoutlem4  15259  lcmfeq0b  15343  lcmfunsnlem2  15353  divgcdcoprmex  15380  prmind2  15398  isprm5  15419  prm23ge5  15520  pcqmul  15558  pcadd  15593  prmreclem2  15621  prmreclem5  15624  mul4sq  15658  vdwmc2  15683  ramcl  15733  prmgaplem7  15761  prmlem1a  15813  setsstruct2  15896  divsfval  16207  iscatd2  16342  catpropd  16369  wunfunc  16559  gaorber  17741  psgneu  17926  lsmsubm  18068  pj1eu  18109  efgredlem  18160  qusabl  18268  cygabl  18292  cygctb  18293  lt6abl  18296  gsumval3eu  18305  dprdsubg  18423  ablfac1c  18470  pgpfac1  18479  dvdsrtr  18652  unitgrp  18667  drngmul0or  18768  lvecvs0or  19108  lspdisjb  19126  lspsolvlem  19142  lspprat  19153  lbsextlem2  19159  abvn0b  19302  domnchr  19880  znfld  19909  cygznlem3  19918  obselocv  20072  cpmatacl  20521  chfacfisf  20659  chfacfisfcpmat  20660  0ntr  20875  opnneiid  20930  restntr  20986  hausnei2  21157  nrmsep3  21159  cmpsub  21203  uncmp  21206  dfconn2  21222  cnconn  21225  1stcfb  21248  txuni2  21368  txbas  21370  ptbasin  21380  txcls  21407  txbasval  21409  txlly  21439  txnlly  21440  pthaus  21441  txlm  21451  tx1stc  21453  xkohaus  21456  isufil2  21712  ufileu  21723  cnpflfi  21803  txflf  21810  fclscf  21829  flimfnfcls  21832  alexsubb  21850  alexsubALTlem2  21852  alexsubALTlem4  21854  ptcmplem2  21857  ptcmplem3  21858  cnextcn  21871  qustgplem  21924  prdsmet  22175  blin2  22234  prdsbl  22296  nmolb  22521  tgqioo  22603  reconnlem2  22630  reconn  22631  lebnumlem3  22762  iscau4  23077  cmetcaulem  23086  iscmet3lem2  23090  bcthlem5  23125  minveclem3b  23199  pmltpc  23219  evthicc2  23229  ovolunlem2  23266  ovolicc2lem5  23289  mblsplit  23300  iundisj2  23317  volsup  23324  ioombl1lem4  23329  dyaddisj  23364  dyadmbllem  23367  i1faddlem  23460  itg10a  23477  itg1ge0a  23478  mbfi1flimlem  23489  mbfmullem  23492  itg2add  23526  rolle  23753  dvcvx  23783  itgsubst  23812  tdeglem4  23820  ply1domn  23883  fta1b  23929  plyadd  23973  plymul  23974  coeeu  23981  vieta1  24067  aalioulem6  24092  ulmcaulem  24148  ulmcau  24149  ulmbdd  24152  ulmcn  24153  amgm  24717  mumullem2  24906  ppiublem1  24927  dchrfi  24980  dchrptlem2  24990  dchrptlem3  24991  dchrsum2  24993  lgsdchr  25080  lgsquad2lem2  25110  2sqlem5  25147  2sqb  25157  pntlemp  25299  ostthlem2  25317  ostth  25328  iscgrglt  25409  tgbtwnconn1  25470  colline  25544  lmimid  25686  axcontlem8  25851  axcontlem9  25852  eengtrkg  25865  structgrssvtxlemOLD  25915  numedglnl  26039  uhgr2edg  26100  uspgr2wlkeq  26542  wlkonl1iedg  26561  wlkdlem2  26580  pthdlem2  26664  clwlkclwwlklem2a4  26898  clwwisshclwwsn  26929  frgr2wwlkeu  27191  frgrreg  27252  frgrregord013  27253  nvmul0or  27505  ubthlem3  27728  axhcompl-zf  27855  hvmul0or  27882  ocnel  28157  pjhthmo  28161  spanuni  28403  spansni  28416  hon0  28652  leopadd  28991  leoptr  28996  mdsymlem6  29267  sumdmdlem2  29278  cdjreui  29291  spc2d  29313  iundisj2f  29403  disjunsn  29407  iundisj2fi  29556  ballotlemimin  30567  bnj23  30784  bnj594  30982  bnj849  30995  txsconn  31223  cvmsdisj  31252  cvmliftlem15  31280  cvmlift2lem10  31294  cvmlift3lem7  31307  mclsppslem  31480  dfon2lem3  31690  dfon2lem5  31692  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  soseq  31751  frr3g  31779  noprefixmo  31848  noetalem3  31865  ifscgr  32151  cgr3tr4  32159  btwnconn1lem13  32206  seglecgr12  32218  elicc3  32311  neibastop1  32354  tailfb  32372  bj-sngltag  32971  bj-elid  33085  mptsnunlem  33185  finxpreclem6  33233  wl-equsal1i  33329  lindsenlbs  33404  poimirlem26  33435  poimirlem27  33436  ismblfin  33450  itg2addnclem3  33463  ftc1anclem6  33490  fdc  33541  riscer  33787  intidl  33828  ispridlc  33869  prtlem14  34159  prtlem17  34161  lpssat  34300  lssatle  34302  lshpkrlem6  34402  cvrnbtwn  34558  atlatmstc  34606  atlatle  34607  atlrelat1  34608  2at0mat0  34811  trlator0  35458  cdleme0moN  35512  cdlemn11pre  36499  dihord2pre  36514  dihmeetlem20N  36615  dochkrshp4  36678  lcfl6  36789  diophin  37336  diophun  37337  pm10.57  38570  fnchoice  39188  ellimcabssub0  39849  fourierdlem81  40404  fourierdlem93  40416  fzopredsuc  41333  2ffzoeq  41338  iccpartlt  41360  cshword2  41437  prmdvdsfmtnof1lem1  41496  lighneallem4  41527  odd2prm2  41627  even3prm2  41628  sbgoldbst  41666  nnsum4primesevenALTV  41689  nzerooringczr  42072  ply1mulgsumlem1  42174  snlindsntor  42260  islininds2  42273  m1modmmod  42316