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

Theorem syl5bi 220
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 197 . 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 187
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 188
This theorem is referenced by:  3imtr4g  273  ancomsd  455  3jao  1325  2euex  2344  2eu1  2354  eqneqall  2638  necon3bd  2643  necon2adOLD  2645  necon1adOLD  2648  pm2.61dne  2748  spcimgft  3163  rspc  3182  rspcimdv  3189  euind  3264  reuind  3281  sbciegft  3336  rspsbc  3384  ssexnelpss  3865  pwpw0  4151  sssn  4161  eqsn  4164  prel12  4180  prnebg  4185  pwsnALT  4217  intss1  4273  intmin  4278  uniintsn  4296  iinss  4353  disji2  4413  disjiun  4417  disjxiun  4423  disjss3  4425  trel3  4528  trin  4530  trintss  4536  eusvnfb  4621  reusv3  4633  copsexg  4707  otiunsndisj  4727  po3nr  4789  fri  4816  wefrc  4848  wereu2  4851  frsn  4925  ssrelrel  4955  relop  5005  iss  5172  restidsing  5181  poirr2  5244  xpcan  5293  xpcan2  5294  sossfld  5303  wfi  5432  wfis2fg  5436  onfr  5481  ord0eln0  5496  onmindif  5531  funopg  5633  funssres  5641  funun  5643  fv3  5894  fvmptt  5981  iinpreima  6025  fvn0ssdmfun  6028  dff3  6050  dff4  6051  fmptsng  6100  fmptsnd  6101  tpres  6132  fnprb  6138  fvclss  6162  isomin  6243  isofrlem  6246  weniso  6260  oprabid  6332  ssorduni  6626  onmindif2  6653  limuni3  6693  tfis2f  6696  tfinds  6700  tfinds2  6704  tfinds3  6705  funcnvuni  6760  f1oweALT  6791  f1o2ndf1  6915  poxp  6919  soxp  6920  fnse  6924  suppimacnv  6936  mpt2xopynvov0g  6968  reldmtpos  6989  rntpos  6994  wfrlem14  7057  wfrlem15  7058  onfununi  7068  smoiun  7088  tfrlem1  7102  tfr3  7125  frsucmptn  7164  tz7.49  7170  oaordi  7255  oawordeulem  7263  omeulem1  7291  oeordi  7296  oelimcl  7309  nnaordi  7327  nneob  7361  omsmolem  7362  erdisj  7419  qsss  7432  uniinqs  7451  map0g  7519  resixpfo  7568  ixpsnf1o  7570  xpdom3  7676  mapdom3  7750  phplem4  7760  php3  7764  unxpdomlem3  7784  ssfi  7798  findcard2  7817  findcard3  7820  frfi  7822  isfiniteg  7837  xpfi  7848  fiint  7854  finsschain  7887  dffi2  7943  marypha1lem  7953  marypha2  7959  supmo  7972  suplub2  7981  ordiso2  8030  ordtypelem7  8039  ordtypelem8  8040  brwdom2  8088  unxpwdom2  8103  ixpiunwdom  8106  elirrv  8112  suc11reg  8124  noinfep  8164  cantnfle  8175  cantnflem1  8193  cantnf  8197  trcl  8211  epfrs  8214  rankpwi  8293  rankunb  8320  rankuni2b  8323  rankxplim3  8351  cplem1  8359  karden  8365  carddom2  8410  fseqenlem2  8454  ac10ct  8463  acni2  8475  acndom  8480  infpwfien  8491  alephordi  8503  alephord  8504  iunfictbso  8543  aceq3lem  8549  dfac5  8557  dfac2  8559  dfac12lem3  8573  dfac12r  8574  cdainflem  8619  cdainf  8620  cfub  8677  cfeq0  8684  coflim  8689  cfslb2n  8696  cofsmo  8697  coftr  8701  infpssr  8736  fin23lem7  8744  fin23lem11  8745  fin23lem21  8767  isf32lem2  8782  isf34lem4  8805  isfin1-2  8813  isfin1-3  8814  fin1a2lem9  8836  fin1a2lem11  8838  fin1a2lem12  8839  fin1a2lem13  8840  domtriomlem  8870  axdc3lem2  8879  axcclem  8885  ac6c4  8909  zorn2lem4  8927  zorn2lem5  8928  zorn2lem7  8930  ttukeylem5  8941  ttukeyg  8945  brdom6disj  8958  fnrndomg  8961  iunfo  8962  iundom2g  8963  ficard  8988  konigthlem  8991  alephval2  8995  pwcfsdom  9006  fpwwe2lem9  9062  fpwwe2lem11  9064  fpwwe2lem12  9065  fpwwe2lem13  9066  pwfseqlem3  9084  gchpwdom  9094  winalim2  9120  gchina  9123  wunex2  9162  tskr1om2  9192  tskxpss  9196  inar1  9199  tskuni  9207  gruun  9230  grudomon  9241  grur1  9244  ltmpi  9328  ltexprlem2  9461  ltexprlem6  9465  reclem2pr  9472  reclem3pr  9473  reclem4pr  9474  suplem1pr  9476  mulgt0sr  9528  supsrlem  9534  axrrecex  9586  axpre-sup  9592  ltlen  9734  negn0  10047  negf1o  10048  mulge0b  10474  supaddc  10574  supadd  10575  supmul1  10576  supmullem1  10577  supmullem2  10578  supmul  10579  infmrclOLD  10593  cju  10605  nnsub  10648  0mnnnnn0  10902  un0addcl  10903  un0mulcl  10904  nn0sub  10920  nn0n0n1ge2b  10933  peano5uzi  11024  eluzuzle  11167  zsupss  11253  qbtwnre  11492  xrsupexmnf  11590  xrinfmexpnf  11591  xrsupsslem  11592  xrinfmsslem  11593  xrub  11597  supxrun  11601  xrinfm0OLD  11627  ixxdisj  11650  icodisj  11755  difreicc  11762  uzsubsubfz  11819  elfzmlbp  11900  fzofzim  11960  elfznelfzo  12011  injresinj  12022  flval3  12047  modirr  12157  ssnn0fi  12194  seqf1o  12251  expcl2lem  12281  expnegz  12303  expaddz  12313  expmulz  12315  facwordi  12471  faclbnd4lem4  12478  bccl  12504  hashnfinnn0  12539  hashgt12el  12590  hashgt12el2  12591  hashfun  12604  hashbclem  12610  hashbc  12611  hashfacen  12612  hashf1lem1  12613  hashf1  12615  hash2pwpr  12628  brfi1uzind  12641  wrdind  12818  wrd2ind  12819  reuccats1  12822  swrdccatin1  12824  swrdccatin2  12828  swrdccat3  12833  swrdccat3blem  12836  cshw1  12906  cshwcsh2id  12912  wwlktovfo  13012  rtrclreclem3  13102  dfrtrcl2  13104  sqrlem1  13285  sqrlem6  13290  rexanre  13388  cau3lem  13396  2clim  13614  summo  13761  fsum2dlem  13809  fsumiun  13859  prodmo  13968  fprod2dlem  14012  bpolycl  14083  rpnnen2  14256  odd2np1lem  14342  bitsfzo  14383  sadcaddlem  14405  gcd0id  14461  algcvgblem  14507  lcmfunsnlem1  14581  lcmfunsnlem2lem1  14582  lcmfunsnlem2  14584  prmdvdsexpr  14640  prmfac1  14642  coprmproddvdslem  14650  qnumdencl  14659  hashdvds  14692  pcneg  14786  prmpwdvds  14811  prmreclem2  14824  4sqlem12  14863  vdwlem6  14899  vdwlem10  14903  vdwlem13  14906  0ram  14941  ram0  14943  ramz  14946  ramcl  14950  prmgaplem3  14986  prmgaplem4  14987  prmgaplem5  14988  prmgaplem6  14989  cshwshashlem1  15029  prmlem0  15040  firest  15290  imasaddfnlem  15385  imasvscafn  15394  mremre  15461  cicsym  15660  initoid  15851  termoid  15852  iszeroi  15855  drsdirfi  16134  pospo  16170  joinfval  16198  meetfval  16212  lubun  16320  odupos  16332  acsfiindd  16374  psss  16411  mnd1id  16530  symgfix2  17008  f1omvdco2  17040  symggen  17062  odcau  17191  pgpfi  17192  sylow2blem3  17209  sylow3lem2  17215  lsmmod  17260  efgsfo  17324  frgpuptinv  17356  frgpnabllem1  17444  cyggeninv  17453  lt6abl  17464  cyggex2  17466  gsumval3lem2  17475  gsumval3  17476  gsum2d2  17541  dmdprdd  17566  dprd2da  17610  pgpfac1lem5  17647  pgpfac  17652  srgbinomlem4  17711  dvdsrtr  17815  dvdsrmul1  17816  lss1d  18121  lspsolvlem  18300  lspsnat  18303  lbsextlem2  18317  lbsextlem3  18318  0ring  18429  01eq0ring  18431  0ring01eqbi  18432  rng1nfld  18437  domnmuln0  18457  abvn0b  18461  mvrf1  18584  mplcoe5lem  18626  opsrtoslem2  18643  cply1mul  18822  coe1fzgsumdlem  18830  gsummoncoe1  18833  pf1ind  18878  evl1gsumdlem  18879  xrsdsreclblem  18949  qsssubdrg  18962  prmirredlem  18995  cygznlem3  19071  obslbs  19224  dsmmacl  19235  lindfrn  19310  lmiclbs  19326  lmisfree  19331  matecl  19381  mat1dimelbas  19427  scmateALT  19468  mdetdiaglem  19554  mdet0  19562  mdetunilem9  19576  gsummatr01  19615  cpmatmcllem  19673  m2cpminvid2lem  19709  pmatcollpw3fi1lem2  19742  chfacfscmul0  19813  chfacfpmmul0  19817  cayhamlem3  19842  unitgOLD  19914  tgcl  19916  tgidm  19927  indistopon  19947  fctop  19950  cctop  19952  ppttop  19953  pptbas  19954  epttop  19955  opnnei  20067  neiptopnei  20079  tgrest  20106  restntr  20129  perfopn  20132  ordtrest2lem  20150  isreg2  20324  lmmo  20327  ordthauslem  20330  cmpsublem  20345  cmpsub  20346  cmpcld  20348  hauscmplem  20352  iunconlem  20373  uncon  20375  2ndcrest  20400  2ndcctbss  20401  2ndcdisj  20402  dis2ndc  20406  locfincmp  20472  comppfsc  20478  txbas  20513  ptbasin  20523  ptbasfi  20527  txcls  20550  txbasval  20552  ptpjopn  20558  ptclsg  20561  dfac14lem  20563  xkoccn  20565  txcnp  20566  txindis  20580  txdis1cn  20581  tx1stc  20596  tx2ndc  20597  txkgen  20598  xkoco1cn  20603  xkoco2cn  20604  xkococn  20606  xkoinjcn  20633  txcon  20635  fbfinnfr  20787  opnfbas  20788  filtop  20801  isfild  20804  fbunfip  20815  filcon  20829  fbasrn  20830  filuni  20831  isufil2  20854  filssufilg  20857  ufileu  20865  filufint  20866  rnelfmlem  20898  rnelfm  20899  fmfnfmlem2  20901  fmfnfmlem4  20903  fmfnfm  20904  hausflimi  20926  hauspwpwf1  20933  flffbas  20941  flftg  20942  alexsublem  20990  alexsubALTlem1  20993  alexsubALTlem2  20994  alexsubALTlem3  20995  alexsubALTlem4  20996  alexsubALT  20997  ptcmplem3  21000  cldsubg  21056  qustgpopn  21065  tgptsmscld  21096  tsmsxplem1  21098  ustfilxp  21158  imasdsf1olem  21319  bldisj  21344  xbln0  21360  prdsxmslem2  21475  xrsblre  21740  icccmplem2  21752  reconn  21757  opnreen  21760  xrge0tsms  21763  metdsre  21781  iccpnfcnv  21868  cnheiborlem  21878  phtpc01  21920  pi1blem  21963  tchcph  22104  cfilfcls  22137  iscau4  22142  bcthlem5  22189  bcth3  22192  hlhil  22278  ovolctb  22321  ovoliunlem2  22334  ovoliunnul  22338  ovolicc2  22353  volfiniun  22377  iundisj  22378  dyadmax  22433  dyadmbllem  22434  vitalilem2  22444  ismbfd  22473  mbfimaopnlem  22488  itg11  22526  i1faddlem  22528  mbfi1fseqlem4  22553  bddmulibl  22673  limciun  22726  perfdvf  22735  rolle  22819  dvivthlem1  22837  dvne0  22840  lhop1  22843  lhop2  22844  itgsubst  22878  dvdsq1p  22986  fta1g  22993  dgrco  23097  plydivex  23118  fta1  23129  ulmcaulem  23214  abelthlem2  23252  pilem2  23272  pilem2OLD  23273  cxpmul2z  23501  cxpcn3lem  23552  xrlimcnp  23759  jensen  23779  wilthlem2  23859  wilthlem3  23860  muval2  23924  sqf11  23929  ppiublem1  23993  fsumvma  24004  lgsdir2lem2  24115  lgsdir2lem5  24118  dchrisum0fno1  24212  pntlem3  24310  pntleml  24312  ostthlem1  24328  ostth2lem2  24335  colinearalg  24786  axcontlem2  24841  axcontlem8  24847  usgrares1  24983  nbgraf1olem5  25018  cusgrarn  25032  nbcusgra  25036  uvtxnbgra  25066  wlkcpr  25102  3v3e3cycl2  25237  usg2wlkeq  25281  wlkiswwlksur  25292  clwlkswlks  25331  clwlkisclwwlklem2a4  25357  clwlkisclwwlklem1  25360  clwwlkf1  25369  erclwwlktr  25388  erclwwlkntr  25400  hashecclwwlkn1  25407  usghashecclwwlk  25408  wlklenvclwlk  25412  clwlkfoclwwlk  25418  vdusgra0nedg  25481  nbhashuvtx  25489  usgravd0nedg  25491  usgravd00  25492  rusgranumwlklem1  25522  3cyclfrgrarn1  25585  frgranbnb  25593  frgrancvvdeqlem3  25605  frgrancvvdeqlem4  25606  frgrancvvdeqlemC  25612  frgrawopreglem3  25619  frgrawopreglem5  25621  frgrawopreg2  25624  2spotiundisj  25635  2spotmdisj  25641  extwwlkfablem2  25651  numclwwlkun  25652  numclwwlkovf2ex  25659  numclwlk1lem2f1  25667  gxnn0neg  25836  gxnn0suc  25837  lnon0  26284  shmodsi  26877  shlub  26902  spanunsni  27067  h1datomi  27069  stm1ri  27732  stadd3i  27736  mdsl1i  27809  cvmdi  27812  superpos  27842  chjatom  27845  chirredi  27882  atcvat4i  27885  sumdmdii  27903  sumdmdlem  27906  cdj3lem2a  27924  cdj3lem3a  27927  cdj3i  27929  disji2f  28026  disjif2  28030  iundisjf  28038  rnmpt2ss  28116  xrge0infss  28181  iundisjfi  28208  nn0min  28222  xrge0tsmsd  28387  cnre2csqima  28556  ordtrest2NEWlem  28567  xrge0iifcnv  28578  lmxrge0  28597  measdivcstOLD  28885  dya2iocuni  28944  omssubadd  28961  eulerpartlems  29019  bnj849  29524  bnj1118  29581  derangenlem  29682  erdszelem9  29710  pconcon  29742  iccllyscon  29761  cvmsval  29777  cvmscld  29784  cvmsss2  29785  cvmopnlem  29789  cvmfolem  29790  cvmliftmolem2  29793  cvmlift2lem10  29823  cvmlift2lem12  29825  cvmlift3lem5  29834  cvmlift3lem8  29837  msubvrs  29986  mthmblem  30006  untsucf  30125  3orel1  30130  3orel2  30131  3orel3  30132  nepss  30138  dfon2lem5  30220  dfon2lem6  30221  dfon2lem7  30222  dfon2lem8  30223  rdgprc  30228  trpredtr  30258  dftrpred3g  30261  trpredrec  30266  frmin  30267  frind  30268  frins2fg  30272  wsuclem  30295  frrlem5e  30309  nodenselem4  30358  nodenselem8  30362  nocvxmin  30365  nofulllem5  30380  funpartfun  30495  altopth1  30517  altopth2  30518  colineardim1  30613  lineext  30628  btwnconn1lem14  30652  brsegle  30660  hilbert1.2  30707  trer  30757  elicc3  30758  finminlem  30759  fneint  30789  fnessref  30798  refssfne  30799  neibastop1  30800  neibastop2lem  30801  neibastop2  30802  fnemeet2  30808  fnejoin2  30810  tailfb  30818  arg-ax  30861  ordtoplem  30880  onsuct0  30886  bj-gl4lem  30962  bj-sngltag  31326  bj-bary1lem1  31461  icorempt2  31488  icoreresf  31489  relowlssretop  31500  fin2so  31635  poimirlem24  31667  poimirlem25  31668  poimirlem26  31669  poimirlem27  31670  poimirlem29  31672  poimirlem30  31673  poimirlem31  31674  mblfinlem1  31680  mblfinlem4  31683  ovoliunnfl  31685  itg2addnclem  31696  itg2addnclem2  31697  areacirc  31740  unirep  31742  filbcmb  31770  fzadd2  31773  sdclem1  31775  fdc  31777  nninfnub  31783  isbnd2  31818  ssbnd  31823  prdsbnd2  31830  cntotbnd  31831  heibor1lem  31844  heiborlem1  31846  heiborlem4  31849  heiborlem6  31851  0idl  31961  intidl  31965  unichnidl  31967  keridl  31968  prnc  32003  ceqsex3OLD  32139  prtlem17  32155  prter2  32160  ax12indn  32222  lsatn0  32273  lsatcmp  32277  lssat  32290  lfl1  32344  lshpsmreu  32383  lkrin  32438  glbconxN  32651  cvrat4  32716  paddasslem17  33109  pmodlem2  33120  dalawlem14  33157  pclclN  33164  pclfinN  33173  pclfinclN  33223  poml4N  33226  osumcllem8N  33236  pexmidlem5N  33247  cdleme32a  33716  cdlemg33b0  33976  tendoeq2  34049  diaelrnN  34321  dihmeetlem1N  34566  dihglblem5apreN  34567  dihglblem2N  34570  dochvalr  34633  dochkrshp  34662  lcfl6  34776  lcfrvalsnN  34817  mapdordlem2  34913  mapdh8b  35056  mapdh9a  35066  hdmap14lem13  35159  eldioph2b  35313  eldiophss  35325  diophren  35364  ctbnfien  35369  rencldnfilem  35371  pellexlem3  35384  pellexlem5  35386  pellex  35388  pell14qrexpcl  35420  pellfundre  35434  pellfundge  35435  pellfundlb  35437  pellfundglb  35438  jm2.19lem4  35552  fnwe2lem2  35614  pwssplit4  35652  hbtlem5  35692  ss2iundf  35889  relexpmulg  35940  relexpxpmin  35947  relexpaddss  35948  dftrcl3  35950  dfrtrcl3  35963  isprm7  36296  onfrALT  36551  ax6e2ndeq  36562  snssiALT  36863  hirstL-ax3  37878  2reurex  37992  iccpartiltu  38125  iccpartigtl  38126  iccpartltu  38128  opoeALTV  38201  opeoALTV  38202  gbegt5  38251  gbogt5  38252  bgoldbwt  38267  bgoldbst  38268  sgoldbalt  38271  nnsum3primesle9  38278  evengpoap3  38283  nnsum4primeseven  38284  nnsum4primesevenALTV  38285  wtgoldbnnsum4prm  38286  bgoldbnnsum3prm  38288  bgoldbtbndlem1  38289  bgoldbtbndlem4  38292  bgoldbtbnd  38293  pfxccat3  38356  pfxccat3a  38359  reuccatpfxs1  38364  elnelall  38369  ralnralall  38370  otiunsndisjX  38377  subsubelfzo0  38410  usgra2pthspth  38420  usgvincvad  38473  usgvincvadALT  38476  usgedgvadf1lem2  38483  usgedgvadf1ALTlem2  38486  usgfis  38515  usgfisALT  38519  mgmpropd  38532  copisnmnd  38566  mgm2mgm  38620  ringrng  38636  c0snmgmhm  38671  ztprmneprm  38887  mndpsuppss  38915  lindslinindimp2lem4  39013  lindslinindsimp2  39015  lindsrng01  39020  snlindsntor  39023  ldepspr  39025  isldepslvec2  39037  suppdm  39063  blen1b  39159  dignn0ldlem  39173  digexp  39178  nn0sumshdiglemB  39191  nn0sumshdiglem1  39192
  Copyright terms: Public domain W3C validator