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, 12-Jan-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  452  3jao  1287  2euex  2297  2eu1  2307  eqneqall  2589  necon3bd  2594  necon2adOLD  2596  necon1adOLD  2599  pm2.61dne  2699  spcimgft  3110  rspc  3129  rspcimdv  3136  euind  3211  reuind  3228  sbciegft  3283  rspsbc  3331  ssexnelpss  3808  pwpw0  4092  sssn  4102  eqsn  4105  prel12  4121  prnebg  4126  pwsnALT  4158  intss1  4214  intmin  4219  uniintsn  4237  iinss  4294  disji2  4354  disjiun  4358  disjxiun  4364  disjss3  4366  trel3  4468  trin  4470  trintss  4476  eusvnfb  4561  reusv3  4573  copsexg  4647  otiunsndisj  4667  po3nr  4728  fri  4755  wefrc  4787  wereu2  4790  onfr  4831  ord0eln0  4846  onmindif  4881  frsn  4984  ssrelrel  5016  relop  5066  iss  5233  restidsing  5242  poirr2  5304  xpcan  5353  xpcan2  5354  sossfld  5363  funopg  5528  funssres  5536  funun  5538  fv3  5787  fvmptt  5873  iinpreima  5919  suppssOLD  5922  fvn0ssdmfun  5924  dff3  5946  dff4  5947  fmptsng  5994  fmptsnd  5995  tpres  6026  fnprb  6032  fvclss  6055  isomin  6134  isofrlem  6137  weniso  6151  oprabid  6223  ssorduni  6520  onmindif2  6546  limuni3  6586  tfis2f  6589  tfinds  6593  tfinds2  6597  tfinds3  6598  funcnvuni  6652  f1oweALT  6683  f1o2ndf1  6807  poxp  6811  soxp  6812  fnse  6816  suppimacnv  6828  mpt2xopynvov0g  6860  reldmtpos  6881  rntpos  6886  onfununi  6930  smoiun  6950  tfrlem1  6963  tfr3  6986  frsucmptn  7022  tz7.49  7028  oaordi  7113  oawordeulem  7121  omeulem1  7149  oeordi  7154  oelimcl  7167  nnaordi  7185  nneob  7219  omsmolem  7220  erdisj  7277  qsss  7290  uniinqs  7309  map0g  7377  resixpfo  7426  ixpsnf1o  7428  xpdom3  7534  mapdom3  7608  phplem4  7618  php3  7622  unxpdomlem3  7642  ssfi  7656  findcard2  7675  findcard3  7678  frfi  7680  isfiniteg  7695  xpfi  7706  fiint  7712  finsschain  7742  dffi2  7798  marypha1lem  7808  marypha2  7814  supmo  7826  suplub2  7835  ordiso2  7855  ordtypelem7  7864  ordtypelem8  7865  brwdom2  7914  unxpwdom2  7929  ixpiunwdom  7932  elirrv  7938  suc11reg  7950  noinfep  7990  cantnfle  8003  cantnflem1  8021  cantnf  8025  cantnfleOLD  8033  cantnflem1OLD  8044  cantnfOLD  8047  trcl  8072  epfrs  8075  rankpwi  8154  rankunb  8181  rankuni2b  8184  rankxplim3  8212  cplem1  8220  karden  8226  carddom2  8271  fseqenlem2  8319  ac10ct  8328  acni2  8340  acndom  8345  infpwfien  8356  alephordi  8368  alephord  8369  iunfictbso  8408  aceq3lem  8414  dfac5  8422  dfac2  8424  dfac12lem3  8438  dfac12r  8439  cdainflem  8484  cdainf  8485  cfub  8542  cfeq0  8549  coflim  8554  cfslb2n  8561  cofsmo  8562  coftr  8566  infpssr  8601  fin23lem7  8609  fin23lem11  8610  fin23lem21  8632  isf32lem2  8647  isf34lem4  8670  isfin1-2  8678  isfin1-3  8679  fin1a2lem9  8701  fin1a2lem11  8703  fin1a2lem12  8704  fin1a2lem13  8705  domtriomlem  8735  axdc3lem2  8744  axcclem  8750  ac6c4  8774  zorn2lem4  8792  zorn2lem5  8793  zorn2lem7  8795  ttukeylem5  8806  ttukeyg  8810  brdom6disj  8823  fnrndomg  8826  iunfo  8827  iundom2g  8828  ficard  8853  konigthlem  8856  alephval2  8860  pwcfsdom  8871  fpwwe2lem9  8927  fpwwe2lem11  8929  fpwwe2lem12  8930  fpwwe2lem13  8931  pwfseqlem3  8949  gchpwdom  8959  winalim2  8985  gchina  8988  wunex2  9027  tskr1om2  9057  tskxpss  9061  inar1  9064  tskuni  9072  gruun  9095  grudomon  9106  grur1  9109  ltmpi  9193  ltexprlem2  9326  ltexprlem6  9330  reclem2pr  9337  reclem3pr  9338  reclem4pr  9339  suplem1pr  9341  mulgt0sr  9393  supsrlem  9399  axrrecex  9451  axpre-sup  9457  ltlen  9597  mulge0b  10329  supmul1  10424  supmullem1  10425  supmullem2  10426  supmul  10427  infmrcl  10438  cju  10448  nnsub  10491  0mnnnnn0  10745  un0addcl  10746  un0mulcl  10747  nn0sub  10763  nn0n0n1ge2b  10777  peano5uzi  10868  eluzuzle  11009  negn0  11087  zsupss  11090  qbtwnre  11319  xrsupexmnf  11417  xrinfmexpnf  11418  xrsupsslem  11419  xrinfmsslem  11420  xrub  11424  supxrun  11428  xrinfm0  11449  ixxdisj  11465  icodisj  11566  difreicc  11573  uzsubsubfz  11628  elfzmlbp  11708  fzofzim  11764  elfznelfzo  11814  injresinj  11825  flval3  11850  modirr  11960  ssnn0fi  11997  seqf1o  12051  expcl2lem  12081  expnegz  12103  expaddz  12113  expmulz  12115  facwordi  12269  faclbnd4lem4  12276  bccl  12302  hashnfinnn0  12334  hashgt12el  12385  hashgt12el2  12386  hashfun  12399  hashbclem  12405  hashbc  12406  hashfacen  12407  hashf1lem1  12408  hashf1  12410  hash2pwpr  12423  brfi1uzind  12436  wrdind  12613  wrd2ind  12614  reuccats1  12617  swrdccatin1  12619  swrdccatin2  12623  swrdccat3  12628  swrdccat3blem  12631  cshw1  12701  cshwcsh2id  12707  wwlktovfo  12807  rtrclreclem3  12895  dfrtrcl2  12897  sqrlem1  13078  sqrlem6  13083  rexanre  13181  cau3lem  13189  2clim  13397  summo  13541  fsum2dlem  13587  fsumiun  13637  prodmo  13745  fprod2dlem  13786  rpnnen2  13961  odd2np1lem  14047  bitsfzo  14087  sadcaddlem  14109  gcd0id  14163  algcvgblem  14208  prmdvdsexpr  14259  prmfac1  14261  qnumdencl  14274  hashdvds  14307  pcneg  14399  prmpwdvds  14424  prmreclem2  14437  4sqlem12  14476  vdwlem6  14506  vdwlem10  14510  vdwlem13  14513  0ram  14540  ram0  14542  ramz  14545  ramcl  14549  cshwshashlem1  14582  prmlem0  14593  firest  14840  imasaddfnlem  14935  imasvscafn  14944  mremre  15011  cicsym  15210  initoid  15401  termoid  15402  iszeroi  15405  drsdirfi  15684  pospo  15720  joinfval  15748  meetfval  15762  lubun  15870  odupos  15882  acsfiindd  15924  psss  15961  mnd1id  16080  symgfix2  16558  f1omvdco2  16590  symggen  16612  odcau  16741  pgpfi  16742  sylow2blem3  16759  sylow3lem2  16765  lsmmod  16810  efgsfo  16874  frgpuptinv  16906  frgpnabllem1  16994  cyggeninv  17003  lt6abl  17014  cyggex2  17016  gsumval3OLD  17025  gsumval3lem2  17027  gsumval3  17028  gsum2d2  17116  dmdprdd  17143  dprd2da  17204  pgpfac1lem5  17243  pgpfac  17248  srgbinomlem4  17307  dvdsrtr  17414  dvdsrmul1  17415  lss1d  17722  lspsolvlem  17901  lspsnat  17904  lbsextlem2  17918  lbsextlem3  17919  0ring  18031  01eq0ring  18033  0ring01eqbi  18034  rng1nfld  18039  domnmuln0  18060  abvn0b  18064  mvrf1  18194  mplcoe5lem  18243  opsrtoslem2  18262  cply1mul  18448  coe1fzgsumdlem  18456  gsummoncoe1  18459  pf1ind  18504  evl1gsumdlem  18505  xrsdsreclblem  18577  qsssubdrg  18590  prmirredlem  18623  cygznlem3  18699  obslbs  18852  dsmmacl  18863  lindfrn  18941  lmiclbs  18957  lmisfree  18962  matecl  19012  mat1dimelbas  19058  scmateALT  19099  mdetdiaglem  19185  mdet0  19193  mdetunilem9  19207  gsummatr01  19246  cpmatmcllem  19304  m2cpminvid2lem  19340  pmatcollpw3fi1lem2  19373  chfacfscmul0  19444  chfacfpmmul0  19448  cayhamlem3  19473  unitgOLD  19554  tgcl  19556  tgidm  19567  indistopon  19587  fctop  19590  cctop  19592  ppttop  19593  pptbas  19594  epttop  19595  opnnei  19707  neiptopnei  19719  tgrest  19746  restntr  19769  perfopn  19772  ordtrest2lem  19790  isreg2  19964  lmmo  19967  ordthauslem  19970  cmpsublem  19985  cmpsub  19986  cmpcld  19988  hauscmplem  19992  iunconlem  20013  uncon  20015  2ndcrest  20040  2ndcctbss  20041  2ndcdisj  20042  dis2ndc  20046  locfincmp  20112  comppfsc  20118  txbas  20153  ptbasin  20163  ptbasfi  20167  txcls  20190  txbasval  20192  ptpjopn  20198  ptclsg  20201  dfac14lem  20203  xkoccn  20205  txcnp  20206  txindis  20220  txdis1cn  20221  tx1stc  20236  tx2ndc  20237  txkgen  20238  xkoco1cn  20243  xkoco2cn  20244  xkococn  20246  xkoinjcn  20273  txcon  20275  fbfinnfr  20427  opnfbas  20428  filtop  20441  isfild  20444  fbunfip  20455  filcon  20469  fbasrn  20470  filuni  20471  isufil2  20494  filssufilg  20497  ufileu  20505  filufint  20506  rnelfmlem  20538  rnelfm  20539  fmfnfmlem2  20541  fmfnfmlem4  20543  fmfnfm  20544  hausflimi  20566  hauspwpwf1  20573  flffbas  20581  flftg  20582  alexsublem  20629  alexsubALTlem1  20632  alexsubALTlem2  20633  alexsubALTlem3  20634  alexsubALTlem4  20635  alexsubALT  20636  ptcmplem3  20639  cldsubg  20694  qustgpopn  20703  tgptsmscld  20738  tsmsxplem1  20740  ustfilxp  20800  imasdsf1olem  20961  bldisj  20986  xbln0  21002  prdsxmslem2  21117  xrsblre  21401  icccmplem2  21413  reconn  21418  opnreen  21421  xrge0tsms  21424  metdsre  21442  iccpnfcnv  21529  cnheiborlem  21539  phtpc01  21581  pi1blem  21624  tchcph  21765  cfilfcls  21798  iscau4  21803  bcthlem5  21852  bcth3  21855  hlhil  21943  ovolctb  21986  ovoliunlem2  21999  ovoliunnul  22003  ovolicc2  22018  volfiniun  22042  iundisj  22043  dyadmax  22092  dyadmbllem  22093  vitalilem2  22103  ismbfd  22132  mbfimaopnlem  22147  itg11  22183  i1faddlem  22185  mbfi1fseqlem4  22210  bddmulibl  22330  limciun  22383  perfdvf  22392  rolle  22476  dvivthlem1  22494  dvne0  22497  lhop1  22500  lhop2  22501  itgsubst  22535  dvdsq1p  22646  fta1g  22653  dgrco  22757  plydivex  22778  fta1  22789  ulmcaulem  22874  abelthlem2  22912  pilem2  22932  cxpmul2z  23159  cxpcn3lem  23208  xrlimcnp  23415  jensen  23435  wilthlem2  23460  wilthlem3  23461  muval2  23525  sqf11  23530  ppiublem1  23594  fsumvma  23605  lgsdir2lem2  23716  lgsdir2lem5  23719  dchrisum0fno1  23813  pntlem3  23911  pntleml  23913  ostthlem1  23929  ostth2lem2  23936  colinearalg  24334  axcontlem2  24389  axcontlem8  24395  usgrares1  24531  nbgraf1olem5  24566  cusgrarn  24580  nbcusgra  24584  uvtxnbgra  24614  wlkcpr  24650  3v3e3cycl2  24785  usg2wlkeq  24829  wlkiswwlksur  24840  clwlkswlks  24879  clwlkisclwwlklem2a4  24905  clwlkisclwwlklem1  24908  clwwlkf1  24917  erclwwlktr  24936  erclwwlkntr  24948  hashecclwwlkn1  24955  usghashecclwwlk  24956  wlklenvclwlk  24960  clwlkfoclwwlk  24966  vdusgra0nedg  25029  nbhashuvtx  25037  usgravd0nedg  25039  usgravd00  25040  rusgranumwlklem1  25070  3cyclfrgrarn1  25133  frgranbnb  25141  frgrancvvdeqlem3  25153  frgrancvvdeqlem4  25154  frgrancvvdeqlemC  25160  frgrawopreglem3  25167  frgrawopreglem5  25169  frgrawopreg2  25172  2spotiundisj  25183  2spotmdisj  25189  extwwlkfablem2  25199  numclwwlkun  25200  numclwwlkovf2ex  25207  numclwlk1lem2f1  25215  gxnn0neg  25382  gxnn0suc  25383  lnon0  25830  shmodsi  26424  shlub  26449  spanunsni  26614  h1datomi  26616  stm1ri  27279  stadd3i  27283  mdsl1i  27356  cvmdi  27359  superpos  27389  chjatom  27392  chirredi  27429  atcvat4i  27432  sumdmdii  27450  sumdmdlem  27453  cdj3lem2a  27471  cdj3lem3a  27474  cdj3i  27476  disji2f  27567  disjif2  27571  iundisjf  27578  rnmpt2ss  27661  xrge0infss  27730  iundisjfi  27754  nn0min  27764  xrge0tsmsd  27929  cnre2csqima  28047  ordtrest2NEWlem  28058  xrge0iifcnv  28069  lmxrge0  28088  measdivcstOLD  28351  dya2iocuni  28410  omssubadd  28427  eulerpartlems  28482  derangenlem  28804  erdszelem9  28832  pconcon  28865  iccllyscon  28884  cvmsval  28900  cvmscld  28907  cvmsss2  28908  cvmopnlem  28912  cvmfolem  28913  cvmliftmolem2  28916  cvmlift2lem10  28946  cvmlift2lem12  28948  cvmlift3lem5  28957  cvmlift3lem8  28960  msubvrs  29109  mthmblem  29129  untsucf  29248  3orel1  29253  3orel2  29254  3orel3  29255  nepss  29261  dfon2lem5  29384  dfon2lem6  29385  dfon2lem7  29386  dfon2lem8  29387  rdgprc  29392  wfi  29452  wfis2fg  29456  trpredtr  29478  dftrpred3g  29481  trpredrec  29486  frmin  29487  frind  29488  frins2fg  29492  wfrlem14  29521  wfrlem15  29522  wsuclem  29546  frrlem5e  29560  nodenselem4  29609  nodenselem8  29613  nocvxmin  29616  nofulllem5  29631  funpartfun  29746  altopth1  29768  altopth2  29769  colineardim1  29864  lineext  29879  btwnconn1lem14  29903  brsegle  29911  hilbert1.2  29958  bpolycl  29967  arg-ax  30034  ordtoplem  30053  onsuct0  30059  fin2so  30205  supaddc  30206  supadd  30207  mblfinlem1  30216  mblfinlem4  30219  ovoliunnfl  30221  itg2addnclem  30232  itg2addnclem2  30233  areacirc  30278  trer  30300  elicc3  30301  finminlem  30302  fneint  30332  fnessref  30341  refssfne  30342  neibastop1  30343  neibastop2lem  30344  neibastop2  30345  fnemeet2  30351  fnejoin2  30353  tailfb  30361  unirep  30369  filbcmb  30397  fzadd2  30400  sdclem1  30402  fdc  30404  nninfnub  30410  isbnd2  30445  ssbnd  30450  prdsbnd2  30457  cntotbnd  30458  heibor1lem  30471  heiborlem1  30473  heiborlem4  30476  heiborlem6  30478  0idl  30588  intidl  30592  unichnidl  30594  keridl  30595  prnc  30630  ceqsex3OLD  30767  prtlem17  30783  prter2  30788  eldioph2b  30861  eldiophss  30873  diophren  30912  ctbnfien  30917  rencldnfilem  30919  pellexlem3  30932  pellexlem5  30934  pellex  30936  pell14qrexpcl  30968  pellfundre  30982  pellfundge  30983  pellfundlb  30985  pellfundglb  30986  jm2.19lem4  31100  fnwe2lem2  31163  pwssplit4  31201  hbtlem5  31245  isprm7  31360  hirstL-ax3  32253  2reurex  32352  opoeALTV  32525  opeoALTV  32526  pfxccat3  32601  pfxccat3a  32604  reuccatpfxs1  32609  elnelall  32614  ralnralall  32615  otiunsndisjX  32622  subsubelfzo0  32659  usgra2pthspth  32669  usgvincvad  32722  usgvincvadALT  32725  usgedgvadf1lem2  32732  usgedgvadf1ALTlem2  32735  usgfis  32764  usgfisALT  32768  mgmpropd  32781  copisnmnd  32815  mgm2mgm  32869  ringrng  32885  c0snmgmhm  32920  ztprmneprm  33136  mndpsuppss  33164  lindslinindimp2lem4  33262  lindslinindsimp2  33264  lindsrng01  33269  snlindsntor  33272  ldepspr  33274  isldepslvec2  33286  suppdm  33312  blen1b  33409  dignn0ldlem  33423  digexp  33428  nn0sumshdiglemB  33441  nn0sumshdiglem1  33442  onfrALT  33661  ax6e2ndeq  33672  snssiALT  33974  bnj849  34330  bnj1118  34387  bj-gl4lem  34530  bj-sngltag  34889  bj-bary1lem1  35024  ax12indn  35086  lsatn0  35137  lsatcmp  35141  lssat  35154  lfl1  35208  lshpsmreu  35247  lkrin  35302  glbconxN  35515  cvrat4  35580  paddasslem17  35973  pmodlem2  35984  dalawlem14  36021  pclclN  36028  pclfinN  36037  pclfinclN  36087  poml4N  36090  osumcllem8N  36100  pexmidlem5N  36111  cdleme32a  36580  cdlemg33b0  36840  tendoeq2  36913  diaelrnN  37185  dihmeetlem1N  37430  dihglblem5apreN  37431  dihglblem2N  37434  dochvalr  37497  dochkrshp  37526  lcfl6  37640  lcfrvalsnN  37681  mapdordlem2  37777  mapdh8b  37920  mapdh9a  37930  hdmap14lem13  38023  relexpaddss  38223  dftrcl3  38231  dfrtrcl3  38232  relexpxpmin  38244  relexpmulg  38246
  Copyright terms: Public domain W3C validator