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

Theorem syl5bi 225
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 199 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 33 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3imtr4g  278  ancomsd  460  3jao  1338  2euex  2384  2eu1  2393  eqneqall  2646  necon3bd  2650  pm2.61dne  2722  spcimgft  3137  rspc  3156  rspcimdv  3163  euind  3237  reuind  3255  sbciegft  3310  rspsbc  3358  ssexnelpss  3843  pwpw0  4133  sssn  4143  eqsn  4146  prel12  4165  prnebg  4171  pwsnALT  4207  intss1  4263  intmin  4268  uniintsn  4286  iinss  4343  disji2  4403  disjiun  4407  disjxiun  4413  disjss3  4415  trel3  4519  trin  4521  trintss  4527  eusvnfb  4613  reusv3  4625  copsexg  4701  otiunsndisj  4721  po3nr  4788  fri  4815  wefrc  4847  wereu2  4850  frsn  4924  ssrelrel  4954  relop  5004  iss  5171  restidsing  5180  poirr2  5243  xpcan  5292  xpcan2  5293  sossfld  5302  wfi  5432  wfis2fg  5436  onfr  5481  ord0eln0  5496  onmindif  5531  funopg  5633  funssres  5641  funun  5643  fv3  5901  fvmptt  5988  iinpreima  6033  fvn0ssdmfun  6036  dff3  6058  dff4  6059  fmptsng  6109  fmptsnd  6110  tpres  6141  fnprb  6147  fntpb  6148  fvclss  6172  isomin  6253  isofrlem  6256  weniso  6270  oprabid  6342  ssorduni  6639  onmindif2  6666  limuni3  6706  tfis2f  6709  tfinds  6713  tfinds2  6717  tfinds3  6718  funcnvuni  6773  f1oweALT  6804  f1o2ndf1  6931  poxp  6935  soxp  6936  fnse  6940  suppimacnv  6952  mpt2xopynvov0g  6987  reldmtpos  7007  rntpos  7012  wfrlem14  7075  wfrlem15  7076  onfununi  7086  smoiun  7106  tfrlem1  7120  tfr3  7143  frsucmptn  7182  tz7.49  7188  oaordi  7273  oawordeulem  7281  omeulem1  7309  oeordi  7314  oelimcl  7327  nnaordi  7345  nneob  7379  omsmolem  7380  erdisj  7437  qsss  7450  uniinqs  7469  map0g  7537  resixpfo  7586  ixpsnf1o  7588  xpdom3  7696  mapdom3  7770  phplem4  7780  php3  7784  unxpdomlem3  7804  ssfi  7818  findcard2  7837  findcard3  7840  frfi  7842  isfiniteg  7857  xpfi  7868  fiint  7874  finsschain  7907  dffi2  7963  marypha1lem  7973  marypha2  7979  supmo  7992  suplub2  8001  infmo  8037  ordiso2  8056  ordtypelem7  8065  ordtypelem8  8066  brwdom2  8114  unxpwdom2  8129  ixpiunwdom  8132  elirrv  8138  suc11reg  8150  noinfep  8191  cantnfle  8202  cantnflem1  8220  cantnf  8224  trcl  8238  epfrs  8241  rankpwi  8320  rankunb  8347  rankuni2b  8350  rankxplim3  8378  cplem1  8386  karden  8392  carddom2  8437  fseqenlem2  8482  ac10ct  8491  acni2  8503  acndom  8508  infpwfien  8519  alephordi  8531  alephord  8532  iunfictbso  8571  aceq3lem  8577  dfac5  8585  dfac2  8587  dfac12lem3  8601  dfac12r  8602  cdainflem  8647  cdainf  8648  cfub  8705  cfeq0  8712  coflim  8717  cfslb2n  8724  cofsmo  8725  coftr  8729  infpssr  8764  fin23lem7  8772  fin23lem11  8773  fin23lem21  8795  isf32lem2  8810  isf34lem4  8833  isfin1-2  8841  isfin1-3  8842  fin1a2lem9  8864  fin1a2lem11  8866  fin1a2lem12  8867  fin1a2lem13  8868  domtriomlem  8898  axdc3lem2  8907  axcclem  8913  ac6c4  8937  zorn2lem4  8955  zorn2lem5  8956  zorn2lem7  8958  ttukeylem5  8969  ttukeyg  8973  brdom6disj  8986  fnrndomg  8989  iunfo  8990  iundom2g  8991  ficard  9016  konigthlem  9019  alephval2  9023  pwcfsdom  9034  fpwwe2lem9  9089  fpwwe2lem11  9091  fpwwe2lem12  9092  fpwwe2lem13  9093  pwfseqlem3  9111  gchpwdom  9121  winalim2  9147  gchina  9150  wunex2  9189  tskr1om2  9219  tskxpss  9223  inar1  9226  tskuni  9234  gruun  9257  grudomon  9268  grur1  9271  ltmpi  9355  ltexprlem2  9488  ltexprlem6  9492  reclem2pr  9499  reclem3pr  9500  reclem4pr  9501  suplem1pr  9503  mulgt0sr  9555  supsrlem  9561  axrrecex  9613  axpre-sup  9619  ltlen  9761  addid0  10067  negn0  10076  negf1o  10077  mulge0b  10503  supaddc  10602  supadd  10603  supmul1  10604  supmullem1  10605  supmullem2  10606  supmul  10607  infmrclOLD  10621  cju  10633  nnsub  10676  0mnnnnn0  10931  un0addcl  10932  un0mulcl  10933  nn0sub  10949  nn0n0n1ge2b  10962  peano5uzi  11053  eluzuzle  11196  zsupss  11282  qbtwnre  11521  xrsupexmnf  11619  xrinfmexpnf  11620  xrsupsslem  11621  xrinfmsslem  11622  xrub  11626  supxrun  11630  xrinfm0OLD  11656  ixxdisj  11679  icodisj  11786  difreicc  11793  uzsubsubfz  11850  elfzmlbp  11932  fzofzim  11993  elfznelfzo  12045  injresinj  12057  flval3  12082  modirr  12192  ssnn0fi  12229  seqf1o  12286  expcl2lem  12316  expnegz  12338  expaddz  12348  expmulz  12350  facwordi  12506  faclbnd4lem4  12513  bccl  12539  hashnfinnn0  12574  hashgt12el  12628  hashgt12el2  12629  hashfun  12642  hashbclem  12648  hashbc  12649  hashfacen  12650  hashf1lem1  12651  hashf1  12653  hash2pwpr  12668  fi1uzind  12683  brfi1indALT  12686  wrdind  12870  wrd2ind  12871  reuccats1  12874  swrdccatin1  12876  swrdccatin2  12880  swrdccat3  12885  swrdccat3blem  12888  cshw1  12958  cshwcsh2id  12964  wwlktovfo  13082  rtrclreclem3  13172  dfrtrcl2  13174  sqrlem1  13355  sqrlem6  13360  rexanre  13458  cau3lem  13466  2clim  13685  summo  13832  fsum2dlem  13880  fsumiun  13930  prodmo  14039  fprod2dlem  14083  bpolycl  14154  rpnnen2  14327  odd2np1lem  14413  bitsfzo  14458  sadcaddlem  14480  gcd0id  14536  algcvgblem  14585  lcmfunsnlem1  14659  lcmfunsnlem2lem1  14660  lcmfunsnlem2  14662  prmdvdsexpr  14718  prmfac1  14720  coprmproddvdslem  14728  qnumdencl  14737  hashdvds  14772  pcneg  14872  prmpwdvds  14897  prmreclem2  14910  4sqlem12  14949  vdwlem6  14985  vdwlem10  14989  vdwlem13  14992  0ram  15027  ram0  15029  ramz  15032  ramcl  15036  prmgaplem3  15072  prmgaplem4  15073  prmgaplem5  15074  prmgaplem6  15075  cshwshashlem1  15115  prmlem0  15126  firest  15380  imasaddfnlem  15483  imasvscafn  15492  mremre  15559  cicsym  15758  initoid  15949  termoid  15950  iszeroi  15953  drsdirfi  16232  pospo  16268  joinfval  16296  meetfval  16310  lubun  16418  odupos  16430  acsfiindd  16472  psss  16509  mnd1id  16628  symgfix2  17106  f1omvdco2  17138  symggen  17160  odcau  17305  pgpfi  17306  sylow2blem3  17323  sylow3lem2  17329  lsmmod  17374  efgsfo  17438  frgpuptinv  17470  frgpnabllem1  17558  cyggeninv  17567  lt6abl  17578  cyggex2  17580  gsumval3lem2  17589  gsumval3  17590  gsum2d2  17655  dmdprdd  17680  dprd2da  17724  pgpfac1lem5  17761  pgpfac  17766  srgbinomlem4  17825  dvdsrtr  17929  dvdsrmul1  17930  lss1d  18235  lspsolvlem  18414  lspsnat  18417  lbsextlem2  18431  lbsextlem3  18432  0ring  18543  01eq0ring  18545  0ring01eqbi  18546  rng1nfld  18551  domnmuln0  18571  abvn0b  18575  mvrf1  18698  mplcoe5lem  18740  opsrtoslem2  18757  cply1mul  18936  coe1fzgsumdlem  18944  gsummoncoe1  18947  pf1ind  18992  evl1gsumdlem  18993  xrsdsreclblem  19063  qsssubdrg  19076  prmirredlem  19113  cygznlem3  19189  obslbs  19342  dsmmacl  19353  lindfrn  19428  lmiclbs  19444  lmisfree  19449  matecl  19499  mat1dimelbas  19545  scmateALT  19586  mdetdiaglem  19672  mdet0  19680  mdetunilem9  19694  gsummatr01  19733  cpmatmcllem  19791  m2cpminvid2lem  19827  pmatcollpw3fi1lem2  19860  chfacfscmul0  19931  chfacfpmmul0  19935  cayhamlem3  19960  unitgOLD  20032  tgcl  20034  tgidm  20045  indistopon  20065  fctop  20068  cctop  20070  ppttop  20071  pptbas  20072  epttop  20073  opnnei  20185  neiptopnei  20197  tgrest  20224  restntr  20247  perfopn  20250  ordtrest2lem  20268  isreg2  20442  lmmo  20445  ordthauslem  20448  cmpsublem  20463  cmpsub  20464  cmpcld  20466  hauscmplem  20470  iunconlem  20491  uncon  20493  2ndcrest  20518  2ndcctbss  20519  2ndcdisj  20520  dis2ndc  20524  locfincmp  20590  comppfsc  20596  txbas  20631  ptbasin  20641  ptbasfi  20645  txcls  20668  txbasval  20670  ptpjopn  20676  ptclsg  20679  dfac14lem  20681  xkoccn  20683  txcnp  20684  txindis  20698  txdis1cn  20699  tx1stc  20714  tx2ndc  20715  txkgen  20716  xkoco1cn  20721  xkoco2cn  20722  xkococn  20724  xkoinjcn  20751  txcon  20753  fbfinnfr  20905  opnfbas  20906  filtop  20919  isfild  20922  fbunfip  20933  filcon  20947  fbasrn  20948  filuni  20949  isufil2  20972  filssufilg  20975  ufileu  20983  filufint  20984  rnelfmlem  21016  rnelfm  21017  fmfnfmlem2  21019  fmfnfmlem4  21021  fmfnfm  21022  hausflimi  21044  hauspwpwf1  21051  flffbas  21059  flftg  21060  alexsublem  21108  alexsubALTlem1  21111  alexsubALTlem2  21112  alexsubALTlem3  21113  alexsubALTlem4  21114  alexsubALT  21115  ptcmplem3  21118  cldsubg  21174  qustgpopn  21183  tgptsmscld  21214  tsmsxplem1  21216  ustfilxp  21276  imasdsf1olem  21437  bldisj  21462  xbln0  21478  prdsxmslem2  21593  xrsblre  21878  icccmplem2  21890  reconn  21895  opnreen  21898  xrge0tsms  21901  metdsre  21919  metdsreOLD  21934  iccpnfcnv  22021  cnheiborlem  22031  phtpc01  22076  pi1blem  22119  tchcph  22260  cfilfcls  22293  iscau4  22298  bcthlem5  22345  bcth3  22348  hlhil  22446  ovolctb  22492  ovoliunlem2  22505  ovoliunnul  22509  ovolicc2  22525  volfiniun  22549  iundisj  22550  dyadmax  22605  dyadmbllem  22606  vitalilem2  22616  ismbfd  22645  mbfimaopnlem  22660  itg11  22698  i1faddlem  22700  mbfi1fseqlem4  22725  bddmulibl  22845  limciun  22898  perfdvf  22907  rolle  22991  dvivthlem1  23009  dvne0  23012  lhop1  23015  lhop2  23016  itgsubst  23050  dvdsq1p  23160  fta1g  23167  dgrco  23278  plydivex  23299  fta1  23310  ulmcaulem  23398  abelthlem2  23436  pilem2  23456  pilem2OLD  23457  cxpmul2z  23685  cxpcn3lem  23736  xrlimcnp  23943  jensen  23963  wilthlem2  24043  wilthlem3  24044  muval2  24110  sqf11  24115  ppiublem1  24179  fsumvma  24190  lgsdir2lem2  24301  lgsdir2lem5  24304  dchrisum0fno1  24398  pntlem3  24496  pntleml  24498  ostthlem1  24514  ostth2lem2  24521  colinearalg  24989  axcontlem2  25044  axcontlem8  25050  usgrares1  25187  nbgraf1olem5  25222  cusgrarn  25236  nbcusgra  25240  uvtxnbgra  25270  wlkcpr  25306  3v3e3cycl2  25441  usg2wlkeq  25485  wlkiswwlksur  25496  clwlkswlks  25535  clwlkisclwwlklem2a4  25561  clwlkisclwwlklem1  25564  clwwlkf1  25573  erclwwlktr  25592  erclwwlkntr  25604  hashecclwwlkn1  25611  usghashecclwwlk  25612  wlklenvclwlk  25616  clwlkfoclwwlk  25622  vdusgra0nedg  25685  nbhashuvtx  25693  usgravd0nedg  25695  usgravd00  25696  rusgranumwlklem1  25726  3cyclfrgrarn1  25789  frgranbnb  25797  frgrancvvdeqlem3  25809  frgrancvvdeqlem4  25810  frgrancvvdeqlemC  25816  frgrawopreglem3  25823  frgrawopreglem5  25825  frgrawopreg2  25828  2spotiundisj  25839  2spotmdisj  25845  extwwlkfablem2  25855  numclwwlkun  25856  numclwwlkovf2ex  25863  numclwlk1lem2f1  25871  gxnn0neg  26040  gxnn0suc  26041  lnon0  26488  shmodsi  27091  shlub  27116  spanunsni  27281  h1datomi  27283  stm1ri  27946  stadd3i  27950  mdsl1i  28023  cvmdi  28026  superpos  28056  chjatom  28059  chirredi  28096  atcvat4i  28099  sumdmdii  28117  sumdmdlem  28120  cdj3lem2a  28138  cdj3lem3a  28141  cdj3i  28143  disji2f  28236  disjif2  28240  iundisjf  28248  rnmpt2ss  28325  xrge0infssOLD  28390  iundisjfi  28421  nn0min  28433  xrge0tsmsd  28597  cnre2csqima  28766  ordtrest2NEWlem  28777  xrge0iifcnv  28788  lmxrge0  28807  measdivcstOLD  29095  dya2iocuni  29154  omssubadd  29177  omssubaddOLD  29181  eulerpartlems  29242  bnj849  29785  bnj1118  29842  derangenlem  29943  erdszelem9  29971  pconcon  30003  iccllyscon  30022  cvmsval  30038  cvmscld  30045  cvmsss2  30046  cvmopnlem  30050  cvmfolem  30051  cvmliftmolem2  30054  cvmlift2lem10  30084  cvmlift2lem12  30086  cvmlift3lem5  30095  cvmlift3lem8  30098  msubvrs  30247  mthmblem  30267  untsucf  30386  3orel1  30391  3orel2  30392  3orel3  30393  nepss  30399  dfon2lem5  30482  dfon2lem6  30483  dfon2lem7  30484  dfon2lem8  30485  rdgprc  30490  trpredtr  30520  dftrpred3g  30523  trpredrec  30528  frmin  30529  frind  30530  frins2fg  30534  wsuclem  30557  frrlem5e  30571  nosepon  30605  nodenselem4  30622  nodenselem8  30626  nocvxmin  30629  nofulllem5  30644  funpartfun  30759  altopth1  30781  altopth2  30782  colineardim1  30877  lineext  30892  btwnconn1lem14  30916  brsegle  30924  hilbert1.2  30971  trer  31021  elicc3  31022  finminlem  31023  fneint  31053  fnessref  31062  refssfne  31063  neibastop1  31064  neibastop2lem  31065  neibastop2  31066  fnemeet2  31072  fnejoin2  31074  tailfb  31082  arg-ax  31125  ordtoplem  31144  onsuct0  31150  bj-gl4lem  31223  bj-sngltag  31622  bj-bary1lem1  31761  icorempt2  31799  icoreresf  31800  relowlssretop  31811  finxpreclem6  31833  fin2so  31977  poimirlem24  32009  poimirlem25  32010  poimirlem26  32011  poimirlem27  32012  poimirlem29  32014  poimirlem30  32015  poimirlem31  32016  mblfinlem1  32022  mblfinlem4  32025  ovoliunnfl  32027  itg2addnclem  32038  itg2addnclem2  32039  areacirc  32082  unirep  32084  filbcmb  32112  fzadd2  32115  sdclem1  32117  fdc  32119  nninfnub  32125  isbnd2  32160  ssbnd  32165  prdsbnd2  32172  cntotbnd  32173  heibor1lem  32186  heiborlem1  32188  heiborlem4  32191  heiborlem6  32193  0idl  32303  intidl  32307  unichnidl  32309  keridl  32310  prnc  32345  prtlem17  32493  prter2  32498  ax12indn  32559  lsatn0  32610  lsatcmp  32614  lssat  32627  lfl1  32681  lshpsmreu  32720  lkrin  32775  glbconxN  32988  cvrat4  33053  paddasslem17  33446  pmodlem2  33457  dalawlem14  33494  pclclN  33501  pclfinN  33510  pclfinclN  33560  poml4N  33563  osumcllem8N  33573  pexmidlem5N  33584  cdleme32a  34053  cdlemg33b0  34313  tendoeq2  34386  diaelrnN  34658  dihmeetlem1N  34903  dihglblem5apreN  34904  dihglblem2N  34907  dochvalr  34970  dochkrshp  34999  lcfl6  35113  lcfrvalsnN  35154  mapdordlem2  35250  mapdh8b  35393  mapdh9a  35403  hdmap14lem13  35496  eldioph2b  35650  eldiophss  35662  diophren  35701  ctbnfien  35706  rencldnfilem  35708  pellexlem3  35720  pellexlem5  35722  pellex  35724  pell14qrexpcl  35758  pellfundre  35774  pellfundge  35775  pellfundlb  35777  pellfundglb  35778  jm2.19lem4  35892  fnwe2lem2  35954  pwssplit4  35992  hbtlem5  36032  ss2iundf  36296  relexpmulg  36347  relexpxpmin  36354  relexpaddss  36355  dftrcl3  36357  dfrtrcl3  36370  isprm7  36704  onfrALT  36959  ax6e2ndeq  36970  snssiALT  37264  hirstL-ax3  38517  2reurex  38640  iccpartiltu  38774  iccpartigtl  38775  iccpartltu  38777  opoeALTV  38850  opeoALTV  38851  gbegt5  38900  gbogt5  38901  bgoldbwt  38916  bgoldbst  38917  sgoldbalt  38920  nnsum3primesle9  38927  evengpoap3  38932  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  wtgoldbnnsum4prm  38935  bgoldbnnsum3prm  38937  bgoldbtbndlem1  38938  bgoldbtbndlem4  38941  bgoldbtbnd  38942  pfxccat3  39007  pfxccat3a  39010  reuccatpfxs1  39015  elnelall  39020  ralnralall  39025  propeqop  39039  iunopeqop  39045  otiunsndisjX  39046  fundmge2nop  39068  fpropnf1  39078  subsubelfzo0  39104  edgupgr  39273  umgrpredgav  39278  ausgrumgri  39302  ausgrusgri  39303  ushgredgedga  39356  ushgredgedgaloop  39358  uhgr0v0e  39364  subumgredg2  39407  uhgrspan1  39425  fusgrfisstep  39445  nbuhgr  39461  nbgr2vtx1edg  39468  nbuhgr2vtx1edgb  39470  uhgrnbgr0nb  39472  edgnbusgreu  39491  nbusgredgeu0  39492  nbusgrf1o0  39493  nbusgrvtxm1uvtx  39528  cusgredg  39542  cplgr1v  39547  cusgrfi  39569  usgredgsscusgredg  39570  uspgrloopnb0  39606  usgrvd0nedg  39620  uhgrvd00  39621  upgr1wlkwlk  39700  lfgrwlkprop  39722  spthdep  39766  upgrwlkdvdelem  39768  usgr2wlkneq  39788  pthdlem1  39792  pthdlem2lem  39793  umgr2adedgspth  39897  usgra2pthspth  39938  usgvincvad  39989  usgvincvadALT  39992  usgedgvadf1lem2  39999  usgedgvadf1ALTlem2  40002  usgfis  40031  usgfisALT  40035  mgmpropd  40048  copisnmnd  40082  mgm2mgm  40136  ringrng  40152  c0snmgmhm  40187  ztprmneprm  40401  mndpsuppss  40429  lindslinindimp2lem4  40527  lindslinindsimp2  40529  lindsrng01  40534  snlindsntor  40537  ldepspr  40539  isldepslvec2  40551  suppdm  40577  blen1b  40672  dignn0ldlem  40686  digexp  40691  nn0sumshdiglemB  40704  nn0sumshdiglem1  40705
  Copyright terms: Public domain W3C validator