MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bir Structured version   Unicode version

Theorem syl5bir 220
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
StepHypRef Expression
1 syl5bir.1 . . 3  |-  ( ps  <->  ph )
21biimpri 208 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186
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 187
This theorem is referenced by:  3imtr3g  271  oplem1  967  nic-ax  1528  19.30  1715  19.33b  1719  hbnt  1924  necon1bd  2623  necon4bdOLD  2628  ssdisj  3821  pssdifn0  3834  disjss3  4396  somo  4780  frminex  4805  sofld  5274  ordelord  5434  unizlim  5528  f0rn0  5755  funopfv  5890  mpteqb  5950  suppssrOLD  6001  fvrnressn  6068  funfvima  6130  fliftfun  6195  weniso  6235  tfinds  6679  tfindsg  6680  tfindes  6682  tfinds2  6683  findsg  6713  frxp  6896  suppssr  6936  rdgsucmptnf  7134  frsucmptn  7143  tz7.49  7149  om00  7263  oewordi  7279  iiner  7422  eroveu  7445  undom  7645  sdomdif  7705  php3  7743  sucdom2  7753  unxpdomlem3  7763  fisseneq  7768  pssnn  7775  ordunifi  7806  isfinite2  7814  fiint  7833  infssuni  7847  ixpfi2  7854  finsschain  7863  ordtypelem10  7988  wofib  8006  wemapsolem  8011  unxpwdom2  8050  inf3lem2  8081  cantnfp1lem3  8133  cantnfp1  8134  cantnfp1lem3OLD  8159  cantnfp1OLD  8160  setind  8199  r1tr  8228  r1ordg  8230  rankelb  8276  rankxplim3  8333  cardlim  8387  infxpenlem  8425  infxpenc2  8433  infxpenc2OLD  8437  dfac5lem4  8541  dfac12k  8561  kmlem13  8576  sornom  8691  fin23lem25  8738  fin23lem21  8753  zorn2lem4  8913  iundom2g  8949  fpwwe2lem12  9051  fpwwe2lem13  9052  pwfseqlem4a  9071  eltsk2g  9161  inttsk  9184  tskord  9190  r1tskina  9192  grudomon  9227  arch  10835  zaddcl  10947  uzm1  11159  xrsupsslem  11553  xrinfmsslem  11554  fsequb  12128  fseqsupubi  12131  ssnn0fi  12137  seqf1o  12194  sq01  12334  swrdccatin1  12766  repsdf2  12808  cshw1  12848  rexanre  13330  rexuzre  13336  cau3lem  13338  o1co  13560  rlimcn2  13564  o1of2  13586  lo1add  13600  lo1mul  13601  climcau  13644  climbdd  13645  caucvgb  13653  summo  13690  isumltss  13813  mertenslem2  13848  prodmolem2  13896  prodmo  13897  bitsfzolem  14295  bitsfzo  14296  bezoutlem4  14390  prmind2  14439  isprm5  14464  pcqmul  14588  pcadd  14619  prmreclem2  14646  prmreclem5  14649  mul4sq  14683  vdwmc2  14708  ramcl  14758  prmlem1a  14803  divsfval  15163  iscatd2  15297  catpropd  15324  wunfunc  15514  gaorber  16672  psgneu  16857  lsmsubm  16999  pj1eu  17040  efgredlem  17091  qusabl  17197  cygabl  17219  cygctb  17220  lt6abl  17223  gsumval3eu  17233  dprdsubg  17393  ablfac1c  17444  pgpfac1  17453  dvdsrtr  17623  unitgrp  17638  drngmul0or  17739  lvecvs0or  18076  lspdisjb  18094  lspsolvlem  18110  lspprat  18121  lbsextlem2  18127  abvn0b  18273  domnchr  18871  znfld  18899  cygznlem3  18908  obselocv  19059  cpmatacl  19511  chfacfisf  19649  chfacfisfcpmat  19650  0ntr  19867  opnneiid  19922  restntr  19978  hausnei2  20149  nrmsep3  20151  cmpsub  20195  uncmp  20198  dfcon2  20214  cnconn  20217  1stcfb  20240  txuni2  20360  txbas  20362  ptbasin  20372  txcls  20399  txbasval  20401  txlly  20431  txnlly  20432  pthaus  20433  txlm  20443  tx1stc  20445  xkohaus  20448  isufil2  20703  ufileu  20714  cnpflfi  20794  txflf  20801  fclscf  20820  flimfnfcls  20823  alexsubb  20840  alexsubALTlem2  20842  alexsubALTlem4  20844  ptcmplem2  20847  ptcmplem3  20848  cnextcn  20861  qustgplem  20913  prdsmet  21167  blin2  21226  prdsbl  21288  nmolb  21518  tgqioo  21599  reconnlem2  21626  reconn  21627  lebnumlem3  21757  iscau4  22012  cmetcaulem  22021  iscmet3lem2  22025  bcthlem5  22061  minveclem3b  22137  pmltpc  22156  evthicc2  22166  ovolunlem2  22203  ovolicc2lem5  22226  mblsplit  22237  iundisj2  22253  volsup  22260  ioombl1lem4  22265  dyaddisj  22299  dyadmbllem  22302  i1faddlem  22394  itg10a  22411  itg1ge0a  22412  mbfi1flimlem  22423  mbfmullem  22426  itg2add  22460  rolle  22685  dvcvx  22715  itgsubst  22744  tdeglem4  22752  ply1domn  22818  fta1b  22864  plyadd  22908  plymul  22909  coeeu  22916  vieta1  23002  aalioulem6  23027  ulmcaulem  23083  ulmcau  23084  ulmbdd  23087  ulmcn  23088  amgm  23648  mumullem2  23837  ppiublem1  23860  dchrfi  23913  dchrptlem2  23923  dchrptlem3  23924  dchrsum2  23926  lgsdchr  24006  lgsquad2lem2  24017  2sqlem5  24026  2sqb  24036  pntlemp  24178  ostthlem2  24196  ostth  24207  tgbtwnconn1  24347  colline  24419  lmimid  24555  axcontlem8  24703  axcontlem9  24704  eengtrkg  24717  usgra2edg  24811  usg2wlkeq  25137  clwlkisclwwlklem2a4  25213  clwwisshclwwn  25237  frgraregord013  25547  nvmul0or  25974  ubthlem3  26215  axhcompl-zf  26342  hvmul0or  26369  ocnel  26643  pjhthmo  26647  spanuni  26889  spansni  26902  hon0  27138  leopadd  27477  leoptr  27482  mdsymlem6  27753  sumdmdlem2  27764  cdjreui  27777  spc2d  27799  iundisj2f  27895  disjunsn  27899  iundisj2fi  28063  ballotlemimin  28963  bnj23  29111  bnj594  29310  bnj849  29323  txscon  29551  cvmsdisj  29580  cvmliftlem15  29608  cvmlift2lem10  29622  cvmlift3lem7  29635  mclsppslem  29808  dfon2lem3  30017  dfon2lem5  30019  dfon2lem6  30020  dfon2lem7  30021  dfon2lem8  30022  soseq  30078  frr3g  30099  nodenselem4  30157  nodenselem5  30158  nobndup  30173  nobnddown  30174  ifscgr  30395  cgr3tr4  30403  btwnconn1lem13  30450  seglecgr12  30462  elicc3  30558  neibastop1  30600  tailfb  30618  bj-sngltag  31119  bj-elid  31177  mptsnunlem  31267  wl-equsal1i  31376  ismblfin  31440  itg2addnclem3  31454  ftc1anclem6  31481  fdc  31533  riscer  31686  intidl  31721  ispridlc  31762  prtlem14  31910  prtlem17  31912  lpssat  32044  lssatle  32046  lshpkrlem6  32146  cvrnbtwn  32302  atlatmstc  32350  atlatle  32351  atlrelat1  32352  2at0mat0  32555  trlator0  33202  cdleme0moN  33256  cdlemn11pre  34243  dihord2pre  34258  dihmeetlem20N  34359  dochkrshp4  34422  lcfl6  34533  diophin  35080  diophun  35081  pm10.57  36137  fnchoice  36797  ellimcabssub0  37004  fourierdlem81  37351  fourierdlem93  37363  fzopredsuc  37684  iccpartlt  37704  bgoldbst  37845  nnsum4primesevenALTV  37862  cshword2  37937  ralnralall  37940  2ffzoeq  37985  nzerooringczr  38404  ply1mulgsumlem1  38510  snlindsntor  38596  islininds2  38609  m1modmmod  38657
  Copyright terms: Public domain W3C validator