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  454  3jao  1290  ax12indn  2259  2euex  2352  2eu1  2362  eqneqall  2650  necon3bd  2655  necon2adOLD  2657  necon1adOLD  2660  pm2.61dne  2760  spcimgft  3171  rspc  3190  rspcimdv  3197  euind  3272  reuind  3289  sbciegft  3344  rspsbc  3403  ssexnelpss  3878  pwpw0  4163  sssn  4173  eqsn  4176  prel12  4192  prnebg  4197  pwsnALT  4229  intss1  4286  intmin  4291  uniintsn  4309  iinss  4366  disji2  4424  disjiun  4427  disjxiun  4434  disjss3  4436  trel3  4538  trin  4540  trintss  4546  eusvnfb  4633  reusv3  4645  copsexg  4722  copsexgOLD  4723  otiunsndisj  4743  po3nr  4804  fri  4831  wefrc  4863  wereu2  4866  onfr  4907  ord0eln0  4922  onmindif  4957  frsn  5060  ssrelrel  5093  relop  5143  iss  5311  restidsing  5320  poirr2  5381  xpcan  5433  xpcan2  5434  sossfld  5444  funopg  5610  funssres  5618  funun  5620  fv3  5869  fvmptt  5956  iinpreima  6002  suppssOLD  6005  fvn0ssdmfun  6007  dff3  6029  dff4  6030  fmptsng  6077  fmptsnd  6078  fnprb  6114  fnprOLD  6115  fvclss  6139  isomin  6218  isofrlem  6221  weniso  6235  oprabid  6308  ssorduni  6606  onmindif2  6632  limuni3  6672  tfis2f  6675  tfinds  6679  tfinds2  6683  tfinds3  6684  funcnvuni  6738  f1oweALT  6769  f1o2ndf1  6893  poxp  6897  soxp  6898  fnse  6902  suppimacnv  6914  mpt2xopynvov0g  6944  reldmtpos  6965  rntpos  6970  onfununi  7014  smoiun  7034  tfrlem1  7047  tfr3  7070  frsucmptn  7106  tz7.49  7112  oaordi  7197  oawordeulem  7205  omeulem1  7233  oeordi  7238  oelimcl  7251  nnaordi  7269  nneob  7303  omsmolem  7304  erdisj  7361  qsss  7374  uniinqs  7393  map0g  7460  resixpfo  7509  ixpsnf1o  7511  xpdom3  7617  mapdom3  7691  phplem4  7701  php3  7705  unxpdomlem3  7728  ssfi  7742  findcard2  7762  findcard3  7765  frfi  7767  isfiniteg  7782  xpfi  7793  fiint  7799  finsschain  7829  dffi2  7885  marypha1lem  7895  marypha2  7901  supmo  7914  suplub2  7923  ordiso2  7943  ordtypelem7  7952  ordtypelem8  7953  brwdom2  8002  unxpwdom2  8017  ixpiunwdom  8020  elirrv  8026  suc11reg  8039  noinfep  8079  cantnfle  8093  cantnflem1  8111  cantnf  8115  cantnfleOLD  8123  cantnflem1OLD  8134  cantnfOLD  8137  trcl  8162  epfrs  8165  rankpwi  8244  rankunb  8271  rankuni2b  8274  rankxplim3  8302  cplem1  8310  karden  8316  carddom2  8361  fseqenlem2  8409  ac10ct  8418  acni2  8430  acndom  8435  infpwfien  8446  alephordi  8458  alephord  8459  iunfictbso  8498  aceq3lem  8504  dfac5  8512  dfac2  8514  dfac12lem3  8528  dfac12r  8529  cdainflem  8574  cdainf  8575  cfub  8632  cfeq0  8639  coflim  8644  cfslb2n  8651  cofsmo  8652  coftr  8656  infpssr  8691  fin23lem7  8699  fin23lem11  8700  fin23lem21  8722  isf32lem2  8737  isf34lem4  8760  isfin1-2  8768  isfin1-3  8769  fin1a2lem9  8791  fin1a2lem11  8793  fin1a2lem12  8794  fin1a2lem13  8795  domtriomlem  8825  axdc3lem2  8834  axcclem  8840  ac6c4  8864  zorn2lem4  8882  zorn2lem5  8883  zorn2lem7  8885  ttukeylem5  8896  ttukeyg  8900  brdom6disj  8913  fnrndomg  8916  iunfo  8917  iundom2g  8918  ficard  8943  konigthlem  8946  alephval2  8950  pwcfsdom  8961  fpwwe2lem9  9019  fpwwe2lem11  9021  fpwwe2lem12  9022  fpwwe2lem13  9023  pwfseqlem3  9041  gchpwdom  9051  winalim2  9077  gchina  9080  wunex2  9119  tskr1om2  9149  tskxpss  9153  inar1  9156  tskuni  9164  gruun  9187  grudomon  9198  grur1  9201  ltmpi  9285  ltexprlem2  9418  ltexprlem6  9422  reclem2pr  9429  reclem3pr  9430  reclem4pr  9431  suplem1pr  9433  mulgt0sr  9485  supsrlem  9491  axrrecex  9543  axpre-sup  9549  ltlen  9689  mulge0b  10419  supmul1  10515  supmullem1  10516  supmullem2  10517  supmul  10518  infmrcl  10529  cju  10539  nnsub  10581  0mnnnnn0  10835  un0addcl  10836  un0mulcl  10837  nn0sub  10853  nn0n0n1ge2b  10867  peano5uzi  10958  eluzuzle  11100  negn0  11179  zsupss  11182  qbtwnre  11409  xrsupexmnf  11507  xrinfmexpnf  11508  xrsupsslem  11509  xrinfmsslem  11510  xrub  11514  supxrun  11518  xrinfm0  11539  ixxdisj  11555  icodisj  11656  difreicc  11663  uzsubsubfz  11718  elfzmlbp  11797  fzofzim  11851  elfznelfzo  11897  injresinj  11908  flval3  11933  modirr  12039  ssnn0fi  12076  seqf1o  12130  expcl2lem  12160  expnegz  12182  expaddz  12192  expmulz  12194  facwordi  12349  faclbnd4lem4  12356  bccl  12382  hashnfinnn0  12414  hashgt12el  12463  hashgt12el2  12464  hashfun  12477  hashbclem  12483  hashbc  12484  hashfacen  12485  hashf1lem1  12486  hashf1  12488  hash2pwpr  12501  brfi1uzind  12514  wrdind  12684  wrd2ind  12685  reuccats1  12688  swrdccatin1  12690  swrdccatin2  12694  swrdccat3  12699  swrdccat3blem  12702  cshw1  12772  cshwcsh2id  12778  wwlktovfo  12878  sqrlem1  13058  sqrlem6  13063  rexanre  13161  cau3lem  13169  2clim  13377  summo  13521  fsum2dlem  13567  fsumiun  13617  prodmo  13725  fprod2dlem  13766  rpnnen2  13941  odd2np1lem  14027  bitsfzo  14067  sadcaddlem  14089  gcd0id  14143  algcvgblem  14188  prmdvdsexpr  14239  prmfac1  14241  qnumdencl  14254  hashdvds  14287  pcneg  14379  prmpwdvds  14404  prmreclem2  14417  4sqlem12  14456  vdwlem6  14486  vdwlem10  14490  vdwlem13  14493  0ram  14520  ram0  14522  ramz  14525  ramcl  14529  cshwshashlem1  14562  prmlem0  14573  firest  14812  imasaddfnlem  14907  imasvscafn  14916  mremre  14983  drsdirfi  15546  pospo  15582  joinfval  15610  meetfval  15624  lubun  15732  odupos  15744  acsfiindd  15786  psss  15823  mnd1id  15942  symgfix2  16420  f1omvdco2  16452  symggen  16474  odcau  16603  pgpfi  16604  sylow2blem3  16621  sylow3lem2  16627  lsmmod  16672  efgsfo  16736  frgpuptinv  16768  frgpnabllem1  16856  cyggeninv  16865  lt6abl  16876  cyggex2  16878  gsumval3OLD  16887  gsumval3lem2  16889  gsumval3  16890  gsum2d2  16981  dmdprdd  17009  dprd2da  17070  pgpfac1lem5  17109  pgpfac  17114  srgbinomlem4  17173  dvdsrtr  17280  dvdsrmul1  17281  lss1d  17588  lspsolvlem  17767  lspsnat  17770  lbsextlem2  17784  lbsextlem3  17785  0ring  17897  01eq0ring  17899  0ring01eqbi  17900  rng1nfld  17905  domnmuln0  17926  abvn0b  17930  mvrf1  18060  mplcoe5lem  18109  opsrtoslem2  18128  cply1mul  18314  coe1fzgsumdlem  18322  gsummoncoe1  18325  pf1ind  18370  evl1gsumdlem  18371  xrsdsreclblem  18443  qsssubdrg  18456  prmirredlem  18501  prmirredlemOLD  18504  cygznlem3  18586  obslbs  18739  dsmmacl  18750  lindfrn  18834  lmiclbs  18850  lmisfree  18855  matecl  18905  mat1dimelbas  18951  scmateALT  18992  mdetdiaglem  19078  mdet0  19086  mdetunilem9  19100  gsummatr01  19139  cpmatmcllem  19197  m2cpminvid2lem  19233  pmatcollpw3fi1lem2  19266  chfacfscmul0  19337  chfacfpmmul0  19341  cayhamlem3  19366  unitgOLD  19447  tgcl  19449  tgidm  19460  indistopon  19480  fctop  19483  cctop  19485  ppttop  19486  pptbas  19487  epttop  19488  opnnei  19599  neiptopnei  19611  tgrest  19638  restntr  19661  perfopn  19664  ordtrest2lem  19682  isreg2  19856  lmmo  19859  ordthauslem  19862  cmpsublem  19877  cmpsub  19878  cmpcld  19880  hauscmplem  19884  bwthOLD  19889  iunconlem  19906  uncon  19908  2ndcrest  19933  2ndcctbss  19934  2ndcdisj  19935  dis2ndc  19939  locfincmp  20005  comppfsc  20011  txbas  20046  ptbasin  20056  ptbasfi  20060  txcls  20083  txbasval  20085  ptpjopn  20091  ptclsg  20094  dfac14lem  20096  xkoccn  20098  txcnp  20099  txindis  20113  txdis1cn  20114  tx1stc  20129  tx2ndc  20130  txkgen  20131  xkoco1cn  20136  xkoco2cn  20137  xkococn  20139  xkoinjcn  20166  txcon  20168  fbfinnfr  20320  opnfbas  20321  filtop  20334  isfild  20337  fbunfip  20348  filcon  20362  fbasrn  20363  filuni  20364  isufil2  20387  filssufilg  20390  ufileu  20398  filufint  20399  rnelfmlem  20431  rnelfm  20432  fmfnfmlem2  20434  fmfnfmlem4  20436  fmfnfm  20437  hausflimi  20459  hauspwpwf1  20466  flffbas  20474  flftg  20475  alexsublem  20522  alexsubALTlem1  20525  alexsubALTlem2  20526  alexsubALTlem3  20527  alexsubALTlem4  20528  alexsubALT  20529  ptcmplem3  20532  cldsubg  20587  qustgpopn  20596  tgptsmscld  20631  tsmsxplem1  20633  ustfilxp  20693  imasdsf1olem  20854  bldisj  20879  xbln0  20895  prdsxmslem2  21010  xrsblre  21294  icccmplem2  21306  reconn  21311  opnreen  21314  xrge0tsms  21317  metdsre  21335  iccpnfcnv  21422  cnheiborlem  21432  phtpc01  21474  pi1blem  21517  tchcph  21658  cfilfcls  21691  iscau4  21696  bcthlem5  21745  bcth3  21748  hlhil  21836  ovolctb  21879  ovoliunlem2  21892  ovoliunnul  21896  ovolicc2  21911  volfiniun  21935  iundisj  21936  dyadmax  21985  dyadmbllem  21986  vitalilem2  21996  ismbfd  22025  mbfimaopnlem  22040  itg11  22076  i1faddlem  22078  mbfi1fseqlem4  22103  bddmulibl  22223  limciun  22276  perfdvf  22285  rolle  22369  dvivthlem1  22387  dvne0  22390  lhop1  22393  lhop2  22394  itgsubst  22428  dvdsq1p  22539  fta1g  22546  dgrco  22650  plydivex  22671  fta1  22682  ulmcaulem  22767  abelthlem2  22805  pilem2  22825  cxpmul2z  23050  cxpcn3lem  23099  xrlimcnp  23276  jensen  23296  wilthlem2  23321  wilthlem3  23322  muval2  23386  sqf11  23391  ppiublem1  23455  fsumvma  23466  lgsdir2lem2  23577  lgsdir2lem5  23580  dchrisum0fno1  23674  pntlem3  23772  pntleml  23774  ostthlem1  23790  ostth2lem2  23797  colinearalg  24191  axcontlem2  24246  axcontlem8  24252  usgrares1  24388  nbgraf1olem5  24423  cusgrarn  24437  nbcusgra  24441  uvtxnbgra  24471  wlkcpr  24507  3v3e3cycl2  24642  usg2wlkeq  24686  wlkiswwlksur  24697  clwlkswlks  24736  clwlkisclwwlklem2a4  24762  clwlkisclwwlklem1  24765  clwwlkf1  24774  erclwwlktr  24793  erclwwlkntr  24805  hashecclwwlkn1  24812  usghashecclwwlk  24813  wlklenvclwlk  24817  clwlkfoclwwlk  24823  vdusgra0nedg  24886  nbhashuvtx  24894  usgravd0nedg  24896  usgravd00  24897  rusgranumwlklem1  24927  3cyclfrgrarn1  24990  frgranbnb  24998  frgrancvvdeqlem3  25010  frgrancvvdeqlem4  25011  frgrancvvdeqlemC  25017  frgrawopreglem3  25024  frgrawopreglem5  25026  frgrawopreg2  25029  2spotiundisj  25040  2spotmdisj  25046  extwwlkfablem2  25056  numclwwlkun  25057  numclwwlkovf2ex  25064  numclwlk1lem2f1  25072  gxnn0neg  25243  gxnn0suc  25244  lnon0  25691  shmodsi  26285  shlub  26310  spanunsni  26475  h1datomi  26477  stm1ri  27141  stadd3i  27145  mdsl1i  27218  cvmdi  27221  superpos  27251  chjatom  27254  chirredi  27291  atcvat4i  27294  sumdmdii  27312  sumdmdlem  27315  cdj3lem2a  27333  cdj3lem3a  27336  cdj3i  27338  disji2f  27416  disjif2  27420  iundisjf  27426  rnmpt2ss  27493  xrge0infss  27558  iundisjfi  27579  nn0min  27589  xrge0tsmsd  27753  cnre2csqima  27871  ordtrest2NEWlem  27882  xrge0iifcnv  27893  lmxrge0  27912  measdivcstOLD  28173  dya2iocuni  28232  eulerpartlems  28277  derangenlem  28593  erdszelem9  28621  pconcon  28654  iccllyscon  28673  cvmsval  28689  cvmscld  28696  cvmsss2  28697  cvmopnlem  28701  cvmfolem  28702  cvmliftmolem2  28705  cvmlift2lem10  28735  cvmlift2lem12  28737  cvmlift3lem5  28746  cvmlift3lem8  28749  msubvrs  28898  mthmblem  28918  rtrclreclem.trans  29047  dfrtrcl2  29049  untsucf  29060  3orel1  29065  3orel2  29066  3orel3  29067  nepss  29073  dfon2lem5  29195  dfon2lem6  29196  dfon2lem7  29197  dfon2lem8  29198  rdgprc  29203  wfi  29263  wfis2fg  29267  trpredtr  29289  dftrpred3g  29292  trpredrec  29297  frmin  29298  frind  29299  frins2fg  29303  wfrlem14  29332  wfrlem15  29333  wsuclem  29357  frrlem5e  29371  nodenselem4  29420  nodenselem8  29424  nocvxmin  29427  nofulllem5  29442  funpartfun  29569  altopth1  29591  altopth2  29592  colineardim1  29687  lineext  29702  btwnconn1lem14  29726  brsegle  29734  hilbert1.2  29781  bpolycl  29790  arg-ax  29857  ordtoplem  29876  onsuct0  29882  fin2so  30016  supaddc  30017  supadd  30018  mblfinlem1  30027  mblfinlem4  30030  ovoliunnfl  30032  itg2addnclem  30042  itg2addnclem2  30043  areacirc  30088  trer  30110  elicc3  30111  finminlem  30112  fneint  30142  fnessref  30151  refssfne  30152  neibastop1  30153  neibastop2lem  30154  neibastop2  30155  fnemeet2  30161  fnejoin2  30163  tailfb  30171  unirep  30179  filbcmb  30207  fzadd2  30210  sdclem1  30212  fdc  30214  nninfnub  30220  isbnd2  30255  ssbnd  30260  prdsbnd2  30267  cntotbnd  30268  heibor1lem  30281  heiborlem1  30283  heiborlem4  30286  heiborlem6  30288  0idl  30398  intidl  30402  unichnidl  30404  keridl  30405  prnc  30440  ceqsex3OLD  30577  prtlem17  30593  prter2  30598  eldioph2b  30672  eldiophss  30684  diophren  30723  ctbnfien  30728  rencldnfilem  30730  pellexlem3  30743  pellexlem5  30745  pellex  30747  pell14qrexpcl  30779  pellfundre  30793  pellfundge  30794  pellfundlb  30796  pellfundglb  30797  jm2.19lem4  30910  fnwe2lem2  30973  pwssplit4  31011  hbtlem5  31053  isprm7  31168  hirstL-ax3  32041  2reurex  32140  elnelall  32247  ralnralall  32248  otiunsndisjX  32255  subsubelfzo0  32292  usgra2pthspth  32305  usgvincvad  32358  usgvincvadALT  32361  usgedgvadf1lem2  32368  usgedgvadf1ALTlem2  32371  usgfis  32400  usgfisALT  32404  mgmpropd  32417  copisnmnd  32450  mgm2mgm  32504  tpres  32506  ringrng  32523  ztprmneprm  32804  mndpsuppss  32834  lindslinindimp2lem4  32932  lindslinindsimp2  32934  lindsrng01  32939  snlindsntor  32942  ldepspr  32944  isldepslvec2  32956  onfrALT  33189  ax6e2ndeq  33200  snssiALT  33496  bnj849  33851  bnj1118  33908  bj-gl4lem  34066  bj-sngltag  34424  bj-bary1lem1  34555  lsatn0  34599  lsatcmp  34603  lssat  34616  lfl1  34670  lshpsmreu  34709  lkrin  34764  glbconxN  34977  cvrat4  35042  paddasslem17  35435  pmodlem2  35446  dalawlem14  35483  pclclN  35490  pclfinN  35499  pclfinclN  35549  poml4N  35552  osumcllem8N  35562  pexmidlem5N  35573  cdleme32a  36042  cdlemg33b0  36302  tendoeq2  36375  diaelrnN  36647  dihmeetlem1N  36892  dihglblem5apreN  36893  dihglblem2N  36896  dochvalr  36959  dochkrshp  36988  lcfl6  37102  lcfrvalsnN  37143  mapdordlem2  37239  mapdh8b  37382  mapdh9a  37392  hdmap14lem13  37485
  Copyright terms: Public domain W3C validator