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

Theorem syl5bi 209
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bi.1  |-  ( ph  <->  ps )
syl5bi.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5bi  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3  |-  ( ph  <->  ps )
21biimpi 187 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 30 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr4g  262  ancomsd  441  3jao  1245  sbequ2  1657  19.9ht  1786  19.9tOLD  1869  ax12olem5OLD  1974  ax11indn  2231  2euex  2312  necon3bd  2589  necon2ad  2600  necon1ad  2619  pm2.61dne  2629  spcimgft  2972  rspc  2991  rspcimdv  2998  euind  3066  reuind  3082  sbciegft  3136  rspsbc  3184  pwpw0  3891  sssn  3902  eqsn  3905  prel12  3919  prnebg  3923  pwsnALT  3954  intss1  4009  intmin  4014  uniintsn  4031  iinss  4085  disji2  4142  disjiun  4145  disjxiun  4152  disjss3  4154  trel3  4253  trin  4255  trintss  4261  copsexg  4385  po3nr  4460  fri  4487  wefrc  4519  wereu2  4522  onfr  4563  ord0eln0  4578  onmindif  4613  eusvnfb  4661  reusv3  4673  ssorduni  4708  onmindif2  4734  limuni3  4774  tfis2f  4777  tfinds  4781  tfinds2  4785  tfinds3  4786  frsn  4890  ssrelrel  4918  relop  4965  iss  5131  poirr2  5200  xpcan  5247  xpcan2  5248  sossfld  5259  funopg  5427  funssres  5435  funun  5437  funcnvuni  5460  fv3  5686  fvmptt  5761  iinpreima  5801  suppss  5804  dff3  5823  dff4  5824  fnpr  5891  fnprOLD  5892  fvclss  5921  isomin  5998  isofrlem  6001  f1oweALT  6015  weniso  6016  oprabid  6046  poxp  6396  soxp  6397  fnse  6401  mpt2xopynvov0g  6403  reldmtpos  6425  rntpos  6430  onfununi  6541  smoiun  6561  tfrlem1  6574  tfr3  6598  frsucmptn  6634  tz7.49  6640  oaordi  6727  oawordeulem  6735  omeulem1  6763  oeordi  6768  oelimcl  6781  nnaordi  6799  nneob  6833  omsmolem  6834  erdisj  6890  qsss  6903  uniinqs  6922  th3qlem1  6948  map0g  6991  resixpfo  7038  ixpsnf1o  7040  xpdom3  7144  mapdom3  7217  phplem4  7227  php3  7231  unxpdomlem3  7253  ssfi  7267  findcard2  7286  findcard3  7288  frfi  7290  isfiniteg  7305  xpfi  7316  fiint  7321  finsschain  7350  dffi2  7365  marypha1lem  7375  marypha2  7381  supmo  7392  suplub2  7401  ordiso2  7419  ordtypelem7  7428  ordtypelem8  7429  brwdom2  7476  unxpwdom2  7491  ixpiunwdom  7494  elirrv  7500  suc11reg  7509  noinfep  7549  cantnfle  7561  cantnflem1  7580  cantnf  7584  trcl  7599  epfrs  7602  rankpwi  7684  rankunb  7711  rankuni2b  7714  rankxplim3  7740  cplem1  7748  karden  7754  carddom2  7799  fseqenlem2  7841  ac10ct  7850  acni2  7862  acndom  7867  infpwfien  7878  alephordi  7890  alephord  7891  iunfictbso  7930  aceq3lem  7936  dfac5  7944  dfac2  7946  dfac12lem3  7960  dfac12r  7961  cdainflem  8006  cdainf  8007  cfub  8064  cfeq0  8071  coflim  8076  cfslb2n  8083  cofsmo  8084  coftr  8088  infpssr  8123  fin23lem7  8131  fin23lem11  8132  fin23lem21  8154  isf32lem2  8169  isf34lem4  8192  isfin1-2  8200  isfin1-3  8201  fin1a2lem9  8223  fin1a2lem11  8225  fin1a2lem12  8226  fin1a2lem13  8227  domtriomlem  8257  axdc3lem2  8266  axcclem  8272  ac6c4  8296  zorn2lem4  8314  zorn2lem5  8315  zorn2lem7  8317  ttukeylem5  8328  ttukeyg  8332  brdom6disj  8345  fnrndomg  8348  iunfo  8349  iundom2g  8350  ficard  8375  konigthlem  8378  alephval2  8382  pwcfsdom  8393  fpwwe2lem9  8448  fpwwe2lem11  8450  fpwwe2lem12  8451  fpwwe2lem13  8452  pwfseqlem3  8470  gchpwdom  8484  winalim2  8506  gchina  8509  wunex2  8548  tskr1om2  8578  tskxpss  8582  inar1  8585  tskuni  8593  gruun  8616  grudomon  8627  grur1  8630  ltmpi  8716  ltexprlem2  8849  ltexprlem6  8853  reclem2pr  8860  reclem3pr  8861  reclem4pr  8862  suplem1pr  8864  mulgt0sr  8915  supsrlem  8921  axrrecex  8973  axpre-sup  8979  ltlen  9110  supmul1  9907  supmullem1  9908  supmullem2  9909  supmul  9910  infmrcl  9921  cju  9930  nnsub  9972  un0addcl  10187  un0mulcl  10188  nn0sub  10204  nn0n0n1ge2b  10215  peano5uzi  10292  negn0  10496  zsupss  10499  qbtwnre  10719  xrsupexmnf  10817  xrinfmexpnf  10818  xrsupsslem  10819  xrinfmsslem  10820  xrub  10824  supxrun  10828  xrinfm0  10849  ixxdisj  10865  icodisj  10956  difreicc  10962  elfznelfzo  11121  injresinj  11129  flval3  11151  modirr  11215  seqf1o  11293  expcl2lem  11322  expnegz  11343  expaddz  11353  expmulz  11355  facwordi  11509  faclbnd4lem4  11516  bccl  11542  hashnfinnn0  11572  hashgt12el  11611  hashgt12el2  11612  hashfun  11629  hashbclem  11630  hashbc  11631  hashfacen  11632  hashf1lem1  11633  hashf1  11635  brfi1uzind  11644  wrdind  11720  sqrlem1  11977  sqrlem6  11982  rexanre  12079  cau3lem  12087  2clim  12295  summo  12440  fsum2dlem  12483  fsumiun  12529  rpnnen2  12754  odd2np1lem  12836  bitsfzo  12876  sadcaddlem  12898  gcd0id  12952  algcvgblem  12997  prmdvdsexpr  13045  prmfac1  13047  qnumdencl  13060  hashdvds  13093  pcneg  13176  prmpwdvds  13201  prmreclem2  13214  4sqlem12  13253  vdwlem6  13283  vdwlem10  13287  vdwlem13  13290  0ram  13317  ram0  13319  ramz  13322  ramcl  13326  prmlem0  13357  firest  13589  imasaddfnlem  13682  imasvscafn  13691  mremre  13758  drsdirfi  14324  pospo  14359  lubun  14479  odupos  14491  acsfiindd  14532  psss  14575  odcau  15167  pgpfi  15168  sylow2blem3  15185  sylow3lem2  15191  lsmmod  15236  efgsfo  15300  frgpuptinv  15332  frgpnabllem1  15413  cyggeninv  15422  lt6abl  15433  cyggex2  15435  gsumval3  15443  gsum2d2  15477  dmdprdd  15489  dprd2da  15529  pgpfac1lem5  15566  pgpfac  15571  dvdsrtr  15686  dvdsrmul1  15687  lss1d  15968  lspsolvlem  16143  lspsnat  16146  lbsextlem2  16160  lbsextlem3  16161  domnmuln0  16287  abvn0b  16291  mvrf1  16418  opsrtoslem2  16474  xrsdsreclblem  16669  qsssubdrg  16683  prmirredlem  16698  cygznlem3  16775  obslbs  16882  unitg  16957  tgcl  16959  tgidm  16970  indistopon  16990  fctop  16993  cctop  16995  ppttop  16996  pptbas  16997  epttop  16998  opnnei  17109  neiptopnei  17121  tgrest  17147  restntr  17170  perfopn  17173  ordtrest2lem  17191  isreg2  17365  lmmo  17368  ordthauslem  17371  cmpsublem  17386  cmpsub  17387  cmpcld  17389  hauscmplem  17393  iunconlem  17413  uncon  17415  2ndcrest  17440  2ndcctbss  17441  2ndcdisj  17442  dis2ndc  17446  txbas  17522  ptbasin  17532  ptbasfi  17536  txcls  17559  txbasval  17561  ptpjopn  17567  ptclsg  17570  dfac14lem  17572  xkoccn  17574  txcnp  17575  txindis  17589  txdis1cn  17590  tx1stc  17605  tx2ndc  17606  txkgen  17607  xkoco1cn  17612  xkoco2cn  17613  xkococn  17615  xkoinjcn  17642  txcon  17644  fbfinnfr  17796  opnfbas  17797  filtop  17810  isfild  17813  fbunfip  17824  filcon  17838  fbasrn  17839  filuni  17840  isufil2  17863  filssufilg  17866  ufileu  17874  filufint  17875  rnelfmlem  17907  rnelfm  17908  fmfnfmlem2  17910  fmfnfmlem4  17912  fmfnfm  17913  hausflimi  17935  hauspwpwf1  17942  flffbas  17950  flftg  17951  alexsublem  17998  alexsubALTlem1  18001  alexsubALTlem2  18002  alexsubALTlem3  18003  alexsubALTlem4  18004  alexsubALT  18005  ptcmplem3  18008  cldsubg  18063  divstgpopn  18072  tgptsmscld  18103  tsmsxplem1  18105  ustfilxp  18165  imasdsf1olem  18313  bldisj  18331  xbln0  18341  prdsxmslem2  18451  xrsblre  18715  icccmplem2  18727  reconn  18732  opnreen  18735  xrge0tsms  18738  metdsre  18756  iccpnfcnv  18842  cnheiborlem  18852  phtpc01  18894  pi1blem  18937  tchcph  19067  cfilfcls  19100  iscau4  19105  bcthlem5  19152  bcth3  19155  hlhil  19213  ovolctb  19255  ovoliunlem2  19268  ovoliunnul  19272  ovolicc2  19287  volfiniun  19310  iundisj  19311  dyadmax  19359  dyadmbllem  19360  vitalilem2  19370  ismbfd  19401  mbfimaopnlem  19416  itg11  19452  i1faddlem  19454  mbfi1fseqlem4  19479  bddmulibl  19599  limciun  19650  perfdvf  19659  rolle  19743  dvivthlem1  19761  dvne0  19764  lhop1  19767  lhop2  19768  itgsubst  19802  pf1ind  19844  dvdsq1p  19952  fta1g  19959  dgrco  20062  plydivex  20083  fta1  20094  ulmcaulem  20179  abelthlem2  20217  pilem2  20237  cxpmul2z  20451  cxpcn3lem  20500  xrlimcnp  20676  jensen  20696  wilthlem2  20721  wilthlem3  20722  muval2  20786  sqf11  20791  ppiublem1  20855  fsumvma  20866  lgsdir2lem2  20977  lgsdir2lem5  20980  dchrisum0fno1  21074  pntlem3  21172  pntleml  21174  ostthlem1  21190  ostth2lem2  21197  usgra2edg  21270  usgrares1  21292  nbgraf1olem5  21323  cusgrarn  21336  nbcusgra  21340  uvtxnbgra  21370  3v3e3cycl2  21501  vdusgra0nedg  21529  usgravd0nedg  21533  gxnn0neg  21701  gxnn0suc  21702  lnon0  22149  shmodsi  22741  shlub  22766  spanunsni  22931  h1datomi  22933  stm1ri  23597  stadd3i  23601  mdsl1i  23674  cvmdi  23677  superpos  23707  chjatom  23710  chirredi  23747  atcvat4i  23750  sumdmdii  23768  sumdmdlem  23771  cdj3lem2a  23789  cdj3lem3a  23792  cdj3i  23794  disji2f  23865  disjif2  23869  iundisjf  23874  rnmpt2ss  23929  iundisjfi  23992  xrge0tsmsd  24054  cnre2csqima  24115  xrge0iifcnv  24125  lmxrge0  24143  measdivcstOLD  24374  dya2iocuni  24429  derangenlem  24638  erdszelem9  24666  pconcon  24699  iccllyscon  24718  cvmsval  24734  cvmscld  24741  cvmsss2  24742  cvmopnlem  24746  cvmfolem  24747  cvmliftmolem2  24750  cvmlift2lem10  24780  cvmlift2lem12  24782  cvmlift3lem5  24791  cvmlift3lem8  24794  rtrclreclem.trans  24927  dfrtrcl2  24929  untsucf  24940  3orel1  24945  3orel2  24946  3orel3  24947  nepss  24956  mulge0b  24972  prodmo  25043  dfon2lem5  25169  dfon2lem6  25170  dfon2lem7  25171  dfon2lem8  25172  rdgprc  25177  wfi  25233  wfis2fg  25237  trpredtr  25259  dftrpred3g  25262  trpredrec  25267  frmin  25268  frind  25269  frins2fg  25273  wfrlem14  25295  wfrlem15  25296  frrlem5e  25315  nodenselem4  25364  nodenselem8  25368  nocvxmin  25371  nofulllem5  25386  funpartfun  25508  altopth1  25526  altopth2  25527  colinearalg  25565  axcontlem2  25620  axcontlem8  25626  colineardim1  25711  lineext  25726  btwnconn1lem14  25750  brsegle  25758  hilbert1.2  25805  bpolycl  25814  arg-ax  25882  ordtoplem  25901  onsuct0  25907  supaddc  25949  supadd  25950  ovoliunnfl  25955  itg2addnclem  25959  itg2addnclem2  25960  itg2addnc  25961  areacirc  25990  trer  26012  elicc3  26013  finminlem  26014  fneint  26050  fnessref  26066  refssfne  26067  locfincmp  26077  comppfsc  26080  neibastop1  26081  neibastop2lem  26082  neibastop2  26083  fnemeet2  26089  fnejoin2  26091  tailfb  26099  unirep  26107  filbcmb  26135  fzadd2  26138  sdclem1  26140  fdc  26142  nninfnub  26148  isbnd2  26185  ssbnd  26190  prdsbnd2  26197  cntotbnd  26198  heibor1lem  26211  heiborlem1  26213  heiborlem4  26216  heiborlem6  26218  0idl  26328  intidl  26332  unichnidl  26334  keridl  26335  prnc  26370  ceqsex3OLD  26402  prtlem17  26418  prter2  26423  eldioph2b  26514  eldiophss  26526  diophren  26567  ctbnfien  26572  rencldnfilem  26574  pellexlem3  26587  pellexlem5  26589  pellex  26591  pell14qrexpcl  26623  pellfundre  26637  pellfundge  26638  pellfundlb  26640  pellfundglb  26641  jm2.19lem4  26756  fnwe2lem2  26819  pwssplit4  26862  dsmmacl  26878  lindfrn  26962  lmiclbs  26978  lmisfree  26983  hbtlem5  27003  f1omvdco2  27062  symggen  27082  hirstL-ax3  27530  2reurex  27629  3cyclfrgrarn1  27767  frgranbnb  27775  frgrancvvdeqlem3  27786  frgrancvvdeqlem4  27787  frgrancvvdeqlemC  27793  frgrawopreglem3  27800  frgrawopreglem4  27801  frgrawopreglem5  27802  frgrawopreg2  27805  onfrALT  27980  a9e2ndeq  27991  snssiALT  28283  bnj849  28636  bnj1118  28693  lubunNEW  29090  lsatn0  29116  lsatcmp  29120  lssat  29133  lfl1  29187  lshpsmreu  29226  lkrin  29281  glbconxN  29494  cvrat4  29559  paddasslem17  29952  pmodlem2  29963  dalawlem14  30000  pclclN  30007  pclfinN  30016  pclfinclN  30066  poml4N  30069  osumcllem8N  30079  pexmidlem5N  30090  cdleme32a  30557  cdlemg33b0  30817  tendoeq2  30890  diaelrnN  31162  dihmeetlem1N  31407  dihglblem5apreN  31408  dihglblem2N  31411  dochvalr  31474  dochkrshp  31503  lcfl6  31617  lcfrvalsnN  31658  mapdordlem2  31754  mapdh8b  31897  mapdh9a  31907  hdmap14lem13  32000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator