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

Theorem syl5bi 217
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 194 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr4g  270  ancomsd  454  3jao  1279  ax12indn  2243  2euex  2351  2mo  2357  necon3bd  2640  necon2ad  2654  necon1ad  2673  pm2.61dne  2683  eqneqall  2700  spcimgft  3043  rspc  3062  rspcimdv  3069  euind  3141  reuind  3157  sbciegft  3212  rspsbc  3271  pwpw0  4016  sssn  4026  eqsn  4029  prel12  4044  prnebg  4049  pwsnALT  4081  intss1  4138  intmin  4143  uniintsn  4160  iinss  4216  disji2  4274  disjiun  4277  disjxiun  4284  disjss3  4286  trel3  4388  trin  4390  trintss  4396  eusvnfb  4483  reusv3  4495  copsexg  4571  copsexgOLD  4572  po3nr  4650  fri  4677  wefrc  4709  wereu2  4712  onfr  4753  ord0eln0  4768  onmindif  4803  frsn  4904  ssrelrel  4935  relop  4985  iss  5149  restidsing  5157  poirr2  5217  xpcan  5269  xpcan2  5270  sossfld  5280  funopg  5445  funssres  5453  funun  5455  fv3  5698  fvmptt  5784  iinpreima  5828  suppssOLD  5831  dff3  5851  dff4  5852  fmptsng  5895  fnprb  5931  fnprOLD  5932  fvclss  5954  isomin  6023  isofrlem  6026  weniso  6040  oprabid  6110  ssorduni  6392  onmindif2  6418  limuni3  6458  tfis2f  6461  tfinds  6465  tfinds2  6469  tfinds3  6470  funcnvuni  6525  f1oweALT  6556  f1o2ndf1  6675  poxp  6679  soxp  6680  fnse  6684  suppimacnv  6696  mpt2xopynvov0g  6726  reldmtpos  6748  rntpos  6753  onfununi  6794  smoiun  6814  tfrlem1  6827  tfr3  6850  frsucmptn  6886  tz7.49  6892  oaordi  6977  oawordeulem  6985  omeulem1  7013  oeordi  7018  oelimcl  7031  nnaordi  7049  nneob  7083  omsmolem  7084  erdisj  7140  qsss  7153  uniinqs  7172  th3qlem1  7198  map0g  7244  resixpfo  7293  ixpsnf1o  7295  xpdom3  7401  mapdom3  7475  phplem4  7485  php3  7489  unxpdomlem3  7511  ssfi  7525  findcard2  7544  findcard3  7547  frfi  7549  isfiniteg  7564  xpfi  7575  fiint  7580  finsschain  7610  dffi2  7665  marypha1lem  7675  marypha2  7681  supmo  7694  suplub2  7703  ordiso2  7721  ordtypelem7  7730  ordtypelem8  7731  brwdom2  7780  unxpwdom2  7795  ixpiunwdom  7798  elirrv  7804  suc11reg  7817  noinfep  7857  cantnfle  7871  cantnflem1  7889  cantnf  7893  cantnfleOLD  7901  cantnflem1OLD  7912  cantnfOLD  7915  trcl  7940  epfrs  7943  rankpwi  8022  rankunb  8049  rankuni2b  8052  rankxplim3  8080  cplem1  8088  karden  8094  carddom2  8139  fseqenlem2  8187  ac10ct  8196  acni2  8208  acndom  8213  infpwfien  8224  alephordi  8236  alephord  8237  iunfictbso  8276  aceq3lem  8282  dfac5  8290  dfac2  8292  dfac12lem3  8306  dfac12r  8307  cdainflem  8352  cdainf  8353  cfub  8410  cfeq0  8417  coflim  8422  cfslb2n  8429  cofsmo  8430  coftr  8434  infpssr  8469  fin23lem7  8477  fin23lem11  8478  fin23lem21  8500  isf32lem2  8515  isf34lem4  8538  isfin1-2  8546  isfin1-3  8547  fin1a2lem9  8569  fin1a2lem11  8571  fin1a2lem12  8572  fin1a2lem13  8573  domtriomlem  8603  axdc3lem2  8612  axcclem  8618  ac6c4  8642  zorn2lem4  8660  zorn2lem5  8661  zorn2lem7  8663  ttukeylem5  8674  ttukeyg  8678  brdom6disj  8691  fnrndomg  8694  iunfo  8695  iundom2g  8696  ficard  8721  konigthlem  8724  alephval2  8728  pwcfsdom  8739  fpwwe2lem9  8797  fpwwe2lem11  8799  fpwwe2lem12  8800  fpwwe2lem13  8801  pwfseqlem3  8819  gchpwdom  8829  winalim2  8855  gchina  8858  wunex2  8897  tskr1om2  8927  tskxpss  8931  inar1  8934  tskuni  8942  gruun  8965  grudomon  8976  grur1  8979  ltmpi  9065  ltexprlem2  9198  ltexprlem6  9202  reclem2pr  9209  reclem3pr  9210  reclem4pr  9211  suplem1pr  9213  mulgt0sr  9264  supsrlem  9270  axrrecex  9322  axpre-sup  9328  ltlen  9468  mulge0b  10191  supmul1  10287  supmullem1  10288  supmullem2  10289  supmul  10290  infmrcl  10301  cju  10310  nnsub  10352  0mnnnnn0  10604  un0addcl  10605  un0mulcl  10606  nn0sub  10622  nn0n0n1ge2b  10636  peano5uzi  10722  uzletr  10861  negn0  10933  zsupss  10936  qbtwnre  11161  xrsupexmnf  11259  xrinfmexpnf  11260  xrsupsslem  11261  xrinfmsslem  11262  xrub  11266  supxrun  11270  xrinfm0  11291  ixxdisj  11307  icodisj  11402  difreicc  11409  uzsubsubfz  11463  elfzmlbp  11483  fzofzim  11585  elfznelfzo  11622  injresinj  11631  flval3  11655  modirr  11761  seqf1o  11839  expcl2lem  11869  expnegz  11890  expaddz  11900  expmulz  11902  facwordi  12057  faclbnd4lem4  12064  bccl  12090  hashnfinnn0  12122  hashgt12el  12165  hashgt12el2  12166  hash2pwpr  12174  hashfun  12191  hashbclem  12197  hashbc  12198  hashfacen  12199  hashf1lem1  12200  hashf1  12202  brfi1uzind  12211  wrdind  12363  wrd2ind  12364  swrdccatin1  12366  swrdccatin2  12370  swrdccat3  12375  swrdccat3blem  12378  cshw1  12448  sqrlem1  12724  sqrlem6  12729  rexanre  12826  cau3lem  12834  2clim  13042  summo  13186  fsum2dlem  13229  fsumiun  13276  rpnnen2  13500  odd2np1lem  13583  bitsfzo  13623  sadcaddlem  13645  gcd0id  13699  algcvgblem  13744  prmdvdsexpr  13794  prmfac1  13796  qnumdencl  13809  hashdvds  13842  pcneg  13932  prmpwdvds  13957  prmreclem2  13970  4sqlem12  14009  vdwlem6  14039  vdwlem10  14043  vdwlem13  14046  0ram  14073  ram0  14075  ramz  14078  ramcl  14082  cshwshashlem1  14114  prmlem0  14125  firest  14363  imasaddfnlem  14458  imasvscafn  14467  mremre  14534  drsdirfi  15100  pospo  15135  joinfval  15163  meetfval  15177  lubun  15285  odupos  15297  acsfiindd  15339  psss  15376  symgfix2  15912  f1omvdco2  15945  symggen  15967  odcau  16094  pgpfi  16095  sylow2blem3  16112  sylow3lem2  16118  lsmmod  16163  efgsfo  16227  frgpuptinv  16259  frgpnabllem1  16342  cyggeninv  16351  lt6abl  16362  cyggex2  16364  gsumval3OLD  16373  gsumval3lem2  16375  gsumval3  16376  gsum2d2  16454  dmdprdd  16469  dprd2da  16529  pgpfac1lem5  16568  pgpfac  16573  srgbinomlem4  16629  dvdsrtr  16732  dvdsrmul1  16733  lss1d  17021  lspsolvlem  17200  lspsnat  17203  lbsextlem2  17217  lbsextlem3  17218  domnmuln0  17347  abvn0b  17351  mvrf1  17475  opsrtoslem2  17541  pf1ind  17764  evl1gsumdlem  17765  xrsdsreclblem  17834  qsssubdrg  17847  prmirredlem  17892  prmirredlemOLD  17895  cygznlem3  17977  obslbs  18130  dsmmacl  18141  lindfrn  18225  lmiclbs  18241  lmisfree  18246  matecl  18301  mdet1  18383  mdetunilem9  18401  gsummatr01  18440  unitg  18547  tgcl  18549  tgidm  18560  indistopon  18580  fctop  18583  cctop  18585  ppttop  18586  pptbas  18587  epttop  18588  opnnei  18699  neiptopnei  18711  tgrest  18738  restntr  18761  perfopn  18764  ordtrest2lem  18782  isreg2  18956  lmmo  18959  ordthauslem  18962  cmpsublem  18977  cmpsub  18978  cmpcld  18980  hauscmplem  18984  bwthOLD  18989  iunconlem  19006  uncon  19008  2ndcrest  19033  2ndcctbss  19034  2ndcdisj  19035  dis2ndc  19039  txbas  19115  ptbasin  19125  ptbasfi  19129  txcls  19152  txbasval  19154  ptpjopn  19160  ptclsg  19163  dfac14lem  19165  xkoccn  19167  txcnp  19168  txindis  19182  txdis1cn  19183  tx1stc  19198  tx2ndc  19199  txkgen  19200  xkoco1cn  19205  xkoco2cn  19206  xkococn  19208  xkoinjcn  19235  txcon  19237  fbfinnfr  19389  opnfbas  19390  filtop  19403  isfild  19406  fbunfip  19417  filcon  19431  fbasrn  19432  filuni  19433  isufil2  19456  filssufilg  19459  ufileu  19467  filufint  19468  rnelfmlem  19500  rnelfm  19501  fmfnfmlem2  19503  fmfnfmlem4  19505  fmfnfm  19506  hausflimi  19528  hauspwpwf1  19535  flffbas  19543  flftg  19544  alexsublem  19591  alexsubALTlem1  19594  alexsubALTlem2  19595  alexsubALTlem3  19596  alexsubALTlem4  19597  alexsubALT  19598  ptcmplem3  19601  cldsubg  19656  divstgpopn  19665  tgptsmscld  19700  tsmsxplem1  19702  ustfilxp  19762  imasdsf1olem  19923  bldisj  19948  xbln0  19964  prdsxmslem2  20079  xrsblre  20363  icccmplem2  20375  reconn  20380  opnreen  20383  xrge0tsms  20386  metdsre  20404  iccpnfcnv  20491  cnheiborlem  20501  phtpc01  20543  pi1blem  20586  tchcph  20727  cfilfcls  20760  iscau4  20765  bcthlem5  20814  bcth3  20817  hlhil  20905  ovolctb  20948  ovoliunlem2  20961  ovoliunnul  20965  ovolicc2  20980  volfiniun  21003  iundisj  21004  dyadmax  21053  dyadmbllem  21054  vitalilem2  21064  ismbfd  21093  mbfimaopnlem  21108  itg11  21144  i1faddlem  21146  mbfi1fseqlem4  21171  bddmulibl  21291  limciun  21344  perfdvf  21353  rolle  21437  dvivthlem1  21455  dvne0  21458  lhop1  21461  lhop2  21462  itgsubst  21496  dvdsq1p  21607  fta1g  21614  dgrco  21717  plydivex  21738  fta1  21749  ulmcaulem  21834  abelthlem2  21872  pilem2  21892  cxpmul2z  22111  cxpcn3lem  22160  xrlimcnp  22337  jensen  22357  wilthlem2  22382  wilthlem3  22383  muval2  22447  sqf11  22452  ppiublem1  22516  fsumvma  22527  lgsdir2lem2  22638  lgsdir2lem5  22641  dchrisum0fno1  22735  pntlem3  22833  pntleml  22835  ostthlem1  22851  ostth2lem2  22858  colinearalg  23107  axcontlem2  23162  axcontlem8  23168  usgra2edg  23252  usgrares1  23274  nbgraf1olem5  23305  cusgrarn  23318  nbcusgra  23322  uvtxnbgra  23352  3v3e3cycl2  23501  vdusgra0nedg  23529  usgravd0nedg  23533  gxnn0neg  23701  gxnn0suc  23702  lnon0  24149  shmodsi  24743  shlub  24768  spanunsni  24933  h1datomi  24935  stm1ri  25599  stadd3i  25603  mdsl1i  25676  cvmdi  25679  superpos  25709  chjatom  25712  chirredi  25749  atcvat4i  25752  sumdmdii  25770  sumdmdlem  25773  cdj3lem2a  25791  cdj3lem3a  25794  cdj3i  25796  disji2f  25872  disjif2  25876  iundisjf  25882  rnmpt2ss  25943  suppss3  25978  xrge0infss  26004  iundisjfi  26031  nn0min  26041  xrge0tsmsd  26204  cnre2csqima  26293  ordtrest2NEWlem  26304  xrge0iifcnv  26315  lmxrge0  26334  measdivcstOLD  26590  dya2iocuni  26650  eulerpartlems  26695  derangenlem  27011  erdszelem9  27039  pconcon  27072  iccllyscon  27091  cvmsval  27107  cvmscld  27114  cvmsss2  27115  cvmopnlem  27119  cvmfolem  27120  cvmliftmolem2  27123  cvmlift2lem10  27153  cvmlift2lem12  27155  cvmlift3lem5  27164  cvmlift3lem8  27167  rtrclreclem.trans  27299  dfrtrcl2  27301  untsucf  27312  3orel1  27317  3orel2  27318  3orel3  27319  nepss  27325  prodmo  27400  fprod2dlem  27442  dfon2lem5  27551  dfon2lem6  27552  dfon2lem7  27553  dfon2lem8  27554  rdgprc  27559  wfi  27619  wfis2fg  27623  trpredtr  27645  dftrpred3g  27648  trpredrec  27653  frmin  27654  frind  27655  frins2fg  27659  wfrlem14  27688  wfrlem15  27689  wsuclem  27713  frrlem5e  27727  nodenselem4  27776  nodenselem8  27780  nocvxmin  27783  nofulllem5  27798  funpartfun  27925  altopth1  27947  altopth2  27948  colineardim1  28043  lineext  28058  btwnconn1lem14  28082  brsegle  28090  hilbert1.2  28137  bpolycl  28146  arg-ax  28214  ordtoplem  28233  onsuct0  28239  wl-lem-mo-recur  28346  fin2so  28369  supaddc  28370  supadd  28371  mblfinlem1  28381  mblfinlem4  28384  ovoliunnfl  28386  itg2addnclem  28396  itg2addnclem2  28397  areacirc  28442  trer  28464  elicc3  28465  finminlem  28466  fneint  28502  fnessref  28518  refssfne  28519  locfincmp  28529  comppfsc  28532  neibastop1  28533  neibastop2lem  28534  neibastop2  28535  fnemeet2  28541  fnejoin2  28543  tailfb  28551  unirep  28559  filbcmb  28587  fzadd2  28590  sdclem1  28592  fdc  28594  nninfnub  28600  isbnd2  28635  ssbnd  28640  prdsbnd2  28647  cntotbnd  28648  heibor1lem  28661  heiborlem1  28663  heiborlem4  28666  heiborlem6  28668  0idl  28778  intidl  28782  unichnidl  28784  keridl  28785  prnc  28820  ceqsex3OLD  28958  prtlem17  28974  prter2  28979  eldioph2b  29054  eldiophss  29066  diophren  29105  ctbnfien  29110  rencldnfilem  29112  pellexlem3  29125  pellexlem5  29127  pellex  29129  pell14qrexpcl  29161  pellfundre  29175  pellfundge  29176  pellfundlb  29178  pellfundglb  29179  jm2.19lem4  29294  fnwe2lem2  29357  pwssplit4  29395  hbtlem5  29437  hirstL-ax3  29859  2reurex  29958  elnelall  30069  ralnralall  30071  otiunsndisj  30085  otiunsndisjX  30086  uzuzle  30143  subsubelfzo0  30163  wwlktovfo  30206  reuccats1  30214  usg2wlkeq  30242  wlkcpr  30243  usgra2pthspth  30248  wlkiswwlksur  30304  clwlkswlks  30376  clwlkisclwwlklem2a4  30399  clwlkisclwwlklem1  30402  clwwlkf1  30411  erclwwlktr0  30432  erclwwlktr  30438  erclwwlkntr  30454  hashecclwwlkn1  30461  usghashecclwwlk  30462  wlkp1lenfislenp  30465  clwlkfoclwwlk  30471  nbhashuvtx  30487  usgravd00  30491  rusgranumwlklem1  30520  3cyclfrgrarn1  30557  frgranbnb  30565  frgrancvvdeqlem3  30578  frgrancvvdeqlem4  30579  frgrancvvdeqlemC  30585  frgrawopreglem3  30592  frgrawopreglem4  30593  frgrawopreglem5  30594  frgrawopreg2  30597  2spotiundisj  30608  2spotmdisj  30614  extwwlkfablem2  30624  numclwwlkun  30625  numclwwlkovf2ex  30632  numclwlk1lem2f1  30640  fmptsnd  30674  ztprmneprm  30691  ssnn0fi  30697  0rng  30726  01eq0rng  30728  mndpsuppss  30735  mat1dimelbas  30790  dmatelnd  30798  dmatmul  30799  mdet0  30822  mdetdiaglem  30824  lindslinindimp2lem4  30884  lindslinindsimp2  30886  lindsrng01  30891  snlindsntor  30894  ldepspr  30896  isldepslvec2  30908  rng1nfld  30916  onfrALT  31144  ax6e2ndeq  31155  snssiALT  31451  bnj849  31805  bnj1118  31862  bj-sngltag  32323  bj-bary1lem1  32442  lsatn0  32484  lsatcmp  32488  lssat  32501  lfl1  32555  lshpsmreu  32594  lkrin  32649  glbconxN  32862  cvrat4  32927  paddasslem17  33320  pmodlem2  33331  dalawlem14  33368  pclclN  33375  pclfinN  33384  pclfinclN  33434  poml4N  33437  osumcllem8N  33447  pexmidlem5N  33458  cdleme32a  33925  cdlemg33b0  34185  tendoeq2  34258  diaelrnN  34530  dihmeetlem1N  34775  dihglblem5apreN  34776  dihglblem2N  34779  dochvalr  34842  dochkrshp  34871  lcfl6  34985  lcfrvalsnN  35026  mapdordlem2  35122  mapdh8b  35265  mapdh9a  35275  hdmap14lem13  35368
  Copyright terms: Public domain W3C validator