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  1280  ax12indn  2251  2euex  2360  2eu1  2371  eqneqall  2657  necon3bd  2660  necon2adOLD  2662  necon1adOLD  2665  pm2.61dne  2765  spcimgft  3144  rspc  3163  rspcimdv  3170  euind  3243  reuind  3260  sbciegft  3315  rspsbc  3374  pwpw0  4119  sssn  4129  eqsn  4132  prel12  4147  prnebg  4152  pwsnALT  4184  intss1  4241  intmin  4246  uniintsn  4263  iinss  4319  disji2  4377  disjiun  4380  disjxiun  4387  disjss3  4389  trel3  4491  trin  4493  trintss  4499  eusvnfb  4586  reusv3  4598  copsexg  4674  copsexgOLD  4675  po3nr  4753  fri  4780  wefrc  4812  wereu2  4815  onfr  4856  ord0eln0  4871  onmindif  4906  frsn  5007  ssrelrel  5038  relop  5088  iss  5252  restidsing  5260  poirr2  5320  xpcan  5372  xpcan2  5373  sossfld  5383  funopg  5548  funssres  5556  funun  5558  fv3  5802  fvmptt  5888  iinpreima  5932  suppssOLD  5935  dff3  5955  dff4  5956  fmptsng  5999  fnprb  6035  fnprOLD  6036  fvclss  6058  isomin  6127  isofrlem  6130  weniso  6144  oprabid  6214  ssorduni  6497  onmindif2  6523  limuni3  6563  tfis2f  6566  tfinds  6570  tfinds2  6574  tfinds3  6575  funcnvuni  6630  f1oweALT  6661  f1o2ndf1  6780  poxp  6784  soxp  6785  fnse  6789  suppimacnv  6801  mpt2xopynvov0g  6831  reldmtpos  6853  rntpos  6858  onfununi  6902  smoiun  6922  tfrlem1  6935  tfr3  6958  frsucmptn  6994  tz7.49  7000  oaordi  7085  oawordeulem  7093  omeulem1  7121  oeordi  7126  oelimcl  7139  nnaordi  7157  nneob  7191  omsmolem  7192  erdisj  7248  qsss  7261  uniinqs  7280  th3qlem1  7306  map0g  7352  resixpfo  7401  ixpsnf1o  7403  xpdom3  7509  mapdom3  7583  phplem4  7593  php3  7597  unxpdomlem3  7620  ssfi  7634  findcard2  7653  findcard3  7656  frfi  7658  isfiniteg  7673  xpfi  7684  fiint  7689  finsschain  7719  dffi2  7774  marypha1lem  7784  marypha2  7790  supmo  7803  suplub2  7812  ordiso2  7830  ordtypelem7  7839  ordtypelem8  7840  brwdom2  7889  unxpwdom2  7904  ixpiunwdom  7907  elirrv  7913  suc11reg  7926  noinfep  7966  cantnfle  7980  cantnflem1  7998  cantnf  8002  cantnfleOLD  8010  cantnflem1OLD  8021  cantnfOLD  8024  trcl  8049  epfrs  8052  rankpwi  8131  rankunb  8158  rankuni2b  8161  rankxplim3  8189  cplem1  8197  karden  8203  carddom2  8248  fseqenlem2  8296  ac10ct  8305  acni2  8317  acndom  8322  infpwfien  8333  alephordi  8345  alephord  8346  iunfictbso  8385  aceq3lem  8391  dfac5  8399  dfac2  8401  dfac12lem3  8415  dfac12r  8416  cdainflem  8461  cdainf  8462  cfub  8519  cfeq0  8526  coflim  8531  cfslb2n  8538  cofsmo  8539  coftr  8543  infpssr  8578  fin23lem7  8586  fin23lem11  8587  fin23lem21  8609  isf32lem2  8624  isf34lem4  8647  isfin1-2  8655  isfin1-3  8656  fin1a2lem9  8678  fin1a2lem11  8680  fin1a2lem12  8681  fin1a2lem13  8682  domtriomlem  8712  axdc3lem2  8721  axcclem  8727  ac6c4  8751  zorn2lem4  8769  zorn2lem5  8770  zorn2lem7  8772  ttukeylem5  8783  ttukeyg  8787  brdom6disj  8800  fnrndomg  8803  iunfo  8804  iundom2g  8805  ficard  8830  konigthlem  8833  alephval2  8837  pwcfsdom  8848  fpwwe2lem9  8906  fpwwe2lem11  8908  fpwwe2lem12  8909  fpwwe2lem13  8910  pwfseqlem3  8928  gchpwdom  8938  winalim2  8964  gchina  8967  wunex2  9006  tskr1om2  9036  tskxpss  9040  inar1  9043  tskuni  9051  gruun  9074  grudomon  9085  grur1  9088  ltmpi  9174  ltexprlem2  9307  ltexprlem6  9311  reclem2pr  9318  reclem3pr  9319  reclem4pr  9320  suplem1pr  9322  mulgt0sr  9373  supsrlem  9379  axrrecex  9431  axpre-sup  9437  ltlen  9577  mulge0b  10300  supmul1  10396  supmullem1  10397  supmullem2  10398  supmul  10399  infmrcl  10410  cju  10419  nnsub  10461  0mnnnnn0  10713  un0addcl  10714  un0mulcl  10715  nn0sub  10731  nn0n0n1ge2b  10745  peano5uzi  10831  uzletr  10970  negn0  11042  zsupss  11045  qbtwnre  11270  xrsupexmnf  11368  xrinfmexpnf  11369  xrsupsslem  11370  xrinfmsslem  11371  xrub  11375  supxrun  11379  xrinfm0  11400  ixxdisj  11416  icodisj  11511  difreicc  11518  uzsubsubfz  11572  elfzmlbp  11592  fzofzim  11694  elfznelfzo  11731  injresinj  11740  flval3  11764  modirr  11870  seqf1o  11948  expcl2lem  11978  expnegz  11999  expaddz  12009  expmulz  12011  facwordi  12166  faclbnd4lem4  12173  bccl  12199  hashnfinnn0  12231  hashgt12el  12275  hashgt12el2  12276  hash2pwpr  12284  hashfun  12301  hashbclem  12307  hashbc  12308  hashfacen  12309  hashf1lem1  12310  hashf1  12312  brfi1uzind  12321  wrdind  12473  wrd2ind  12474  swrdccatin1  12476  swrdccatin2  12480  swrdccat3  12485  swrdccat3blem  12488  cshw1  12558  sqrlem1  12834  sqrlem6  12839  rexanre  12936  cau3lem  12944  2clim  13152  summo  13296  fsum2dlem  13339  fsumiun  13386  rpnnen2  13610  odd2np1lem  13693  bitsfzo  13733  sadcaddlem  13755  gcd0id  13809  algcvgblem  13854  prmdvdsexpr  13904  prmfac1  13906  qnumdencl  13919  hashdvds  13952  pcneg  14042  prmpwdvds  14067  prmreclem2  14080  4sqlem12  14119  vdwlem6  14149  vdwlem10  14153  vdwlem13  14156  0ram  14183  ram0  14185  ramz  14188  ramcl  14192  cshwshashlem1  14224  prmlem0  14235  firest  14473  imasaddfnlem  14568  imasvscafn  14577  mremre  14644  drsdirfi  15210  pospo  15245  joinfval  15273  meetfval  15287  lubun  15395  odupos  15407  acsfiindd  15449  psss  15486  symgfix2  16023  f1omvdco2  16056  symggen  16078  odcau  16207  pgpfi  16208  sylow2blem3  16225  sylow3lem2  16231  lsmmod  16276  efgsfo  16340  frgpuptinv  16372  frgpnabllem1  16455  cyggeninv  16464  lt6abl  16475  cyggex2  16477  gsumval3OLD  16486  gsumval3lem2  16488  gsumval3  16489  gsum2d2  16571  dmdprdd  16586  dprd2da  16646  pgpfac1lem5  16685  pgpfac  16690  srgbinomlem4  16747  dvdsrtr  16850  dvdsrmul1  16851  lss1d  17150  lspsolvlem  17329  lspsnat  17332  lbsextlem2  17346  lbsextlem3  17347  domnmuln0  17476  abvn0b  17480  mvrf1  17605  mplcoe5lem  17654  opsrtoslem2  17673  pf1ind  17898  evl1gsumdlem  17899  xrsdsreclblem  17968  qsssubdrg  17981  prmirredlem  18026  prmirredlemOLD  18029  cygznlem3  18111  obslbs  18264  dsmmacl  18275  lindfrn  18359  lmiclbs  18375  lmisfree  18380  matecl  18435  mdetdiaglem  18520  mdet0  18528  mdetunilem9  18542  gsummatr01  18581  unitg  18688  tgcl  18690  tgidm  18701  indistopon  18721  fctop  18724  cctop  18726  ppttop  18727  pptbas  18728  epttop  18729  opnnei  18840  neiptopnei  18852  tgrest  18879  restntr  18902  perfopn  18905  ordtrest2lem  18923  isreg2  19097  lmmo  19100  ordthauslem  19103  cmpsublem  19118  cmpsub  19119  cmpcld  19121  hauscmplem  19125  bwthOLD  19130  iunconlem  19147  uncon  19149  2ndcrest  19174  2ndcctbss  19175  2ndcdisj  19176  dis2ndc  19180  txbas  19256  ptbasin  19266  ptbasfi  19270  txcls  19293  txbasval  19295  ptpjopn  19301  ptclsg  19304  dfac14lem  19306  xkoccn  19308  txcnp  19309  txindis  19323  txdis1cn  19324  tx1stc  19339  tx2ndc  19340  txkgen  19341  xkoco1cn  19346  xkoco2cn  19347  xkococn  19349  xkoinjcn  19376  txcon  19378  fbfinnfr  19530  opnfbas  19531  filtop  19544  isfild  19547  fbunfip  19558  filcon  19572  fbasrn  19573  filuni  19574  isufil2  19597  filssufilg  19600  ufileu  19608  filufint  19609  rnelfmlem  19641  rnelfm  19642  fmfnfmlem2  19644  fmfnfmlem4  19646  fmfnfm  19647  hausflimi  19669  hauspwpwf1  19676  flffbas  19684  flftg  19685  alexsublem  19732  alexsubALTlem1  19735  alexsubALTlem2  19736  alexsubALTlem3  19737  alexsubALTlem4  19738  alexsubALT  19739  ptcmplem3  19742  cldsubg  19797  divstgpopn  19806  tgptsmscld  19841  tsmsxplem1  19843  ustfilxp  19903  imasdsf1olem  20064  bldisj  20089  xbln0  20105  prdsxmslem2  20220  xrsblre  20504  icccmplem2  20516  reconn  20521  opnreen  20524  xrge0tsms  20527  metdsre  20545  iccpnfcnv  20632  cnheiborlem  20642  phtpc01  20684  pi1blem  20727  tchcph  20868  cfilfcls  20901  iscau4  20906  bcthlem5  20955  bcth3  20958  hlhil  21046  ovolctb  21089  ovoliunlem2  21102  ovoliunnul  21106  ovolicc2  21121  volfiniun  21144  iundisj  21145  dyadmax  21194  dyadmbllem  21195  vitalilem2  21205  ismbfd  21234  mbfimaopnlem  21249  itg11  21285  i1faddlem  21287  mbfi1fseqlem4  21312  bddmulibl  21432  limciun  21485  perfdvf  21494  rolle  21578  dvivthlem1  21596  dvne0  21599  lhop1  21602  lhop2  21603  itgsubst  21637  dvdsq1p  21748  fta1g  21755  dgrco  21858  plydivex  21879  fta1  21890  ulmcaulem  21975  abelthlem2  22013  pilem2  22033  cxpmul2z  22252  cxpcn3lem  22301  xrlimcnp  22478  jensen  22498  wilthlem2  22523  wilthlem3  22524  muval2  22588  sqf11  22593  ppiublem1  22657  fsumvma  22668  lgsdir2lem2  22779  lgsdir2lem5  22782  dchrisum0fno1  22876  pntlem3  22974  pntleml  22976  ostthlem1  22992  ostth2lem2  22999  colinearalg  23291  axcontlem2  23346  axcontlem8  23352  usgra2edg  23436  usgrares1  23458  nbgraf1olem5  23489  cusgrarn  23502  nbcusgra  23506  uvtxnbgra  23536  3v3e3cycl2  23685  vdusgra0nedg  23713  usgravd0nedg  23717  gxnn0neg  23885  gxnn0suc  23886  lnon0  24333  shmodsi  24927  shlub  24952  spanunsni  25117  h1datomi  25119  stm1ri  25783  stadd3i  25787  mdsl1i  25860  cvmdi  25863  superpos  25893  chjatom  25896  chirredi  25933  atcvat4i  25936  sumdmdii  25954  sumdmdlem  25957  cdj3lem2a  25975  cdj3lem3a  25978  cdj3i  25980  disji2f  26055  disjif2  26059  iundisjf  26065  rnmpt2ss  26126  suppss3  26161  xrge0infss  26187  iundisjfi  26214  nn0min  26224  xrge0tsmsd  26387  cnre2csqima  26475  ordtrest2NEWlem  26486  xrge0iifcnv  26497  lmxrge0  26516  measdivcstOLD  26772  dya2iocuni  26832  eulerpartlems  26877  derangenlem  27193  erdszelem9  27221  pconcon  27254  iccllyscon  27273  cvmsval  27289  cvmscld  27296  cvmsss2  27297  cvmopnlem  27301  cvmfolem  27302  cvmliftmolem2  27305  cvmlift2lem10  27335  cvmlift2lem12  27337  cvmlift3lem5  27346  cvmlift3lem8  27349  rtrclreclem.trans  27482  dfrtrcl2  27484  untsucf  27495  3orel1  27500  3orel2  27501  3orel3  27502  nepss  27508  prodmo  27583  fprod2dlem  27625  dfon2lem5  27734  dfon2lem6  27735  dfon2lem7  27736  dfon2lem8  27737  rdgprc  27742  wfi  27802  wfis2fg  27806  trpredtr  27828  dftrpred3g  27831  trpredrec  27836  frmin  27837  frind  27838  frins2fg  27842  wfrlem14  27871  wfrlem15  27872  wsuclem  27896  frrlem5e  27910  nodenselem4  27959  nodenselem8  27963  nocvxmin  27966  nofulllem5  27981  funpartfun  28108  altopth1  28130  altopth2  28131  colineardim1  28226  lineext  28241  btwnconn1lem14  28265  brsegle  28273  hilbert1.2  28320  bpolycl  28329  arg-ax  28396  ordtoplem  28415  onsuct0  28421  fin2so  28554  supaddc  28555  supadd  28556  mblfinlem1  28566  mblfinlem4  28569  ovoliunnfl  28571  itg2addnclem  28581  itg2addnclem2  28582  areacirc  28627  trer  28649  elicc3  28650  finminlem  28651  fneint  28687  fnessref  28703  refssfne  28704  locfincmp  28714  comppfsc  28717  neibastop1  28718  neibastop2lem  28719  neibastop2  28720  fnemeet2  28726  fnejoin2  28728  tailfb  28736  unirep  28744  filbcmb  28772  fzadd2  28775  sdclem1  28777  fdc  28779  nninfnub  28785  isbnd2  28820  ssbnd  28825  prdsbnd2  28832  cntotbnd  28833  heibor1lem  28846  heiborlem1  28848  heiborlem4  28851  heiborlem6  28853  0idl  28963  intidl  28967  unichnidl  28969  keridl  28970  prnc  29005  ceqsex3OLD  29143  prtlem17  29159  prter2  29164  eldioph2b  29239  eldiophss  29251  diophren  29290  ctbnfien  29295  rencldnfilem  29297  pellexlem3  29310  pellexlem5  29312  pellex  29314  pell14qrexpcl  29346  pellfundre  29360  pellfundge  29361  pellfundlb  29363  pellfundglb  29364  jm2.19lem4  29479  fnwe2lem2  29542  pwssplit4  29580  hbtlem5  29622  hirstL-ax3  30044  2reurex  30143  elnelall  30254  ralnralall  30256  otiunsndisj  30270  otiunsndisjX  30271  uzuzle  30328  subsubelfzo0  30348  wwlktovfo  30391  reuccats1  30399  usg2wlkeq  30427  wlkcpr  30428  usgra2pthspth  30433  wlkiswwlksur  30489  clwlkswlks  30561  clwlkisclwwlklem2a4  30584  clwlkisclwwlklem1  30587  clwwlkf1  30596  erclwwlktr0  30617  erclwwlktr  30623  erclwwlkntr  30639  hashecclwwlkn1  30646  usghashecclwwlk  30647  wlkp1lenfislenp  30650  clwlkfoclwwlk  30656  nbhashuvtx  30672  usgravd00  30676  rusgranumwlklem1  30705  3cyclfrgrarn1  30742  frgranbnb  30750  frgrancvvdeqlem3  30763  frgrancvvdeqlem4  30764  frgrancvvdeqlemC  30770  frgrawopreglem3  30777  frgrawopreglem4  30778  frgrawopreglem5  30779  frgrawopreg2  30782  2spotiundisj  30793  2spotmdisj  30799  extwwlkfablem2  30809  numclwwlkun  30810  numclwwlkovf2ex  30817  numclwlk1lem2f1  30825  fmptsnd  30860  ztprmneprm  30877  ssnn0fi  30884  0rng  30913  01eq0rng  30915  mndpsuppss  30922  coe1fzgsumdlem  30979  gsummoncoe1  30985  cply1mul  30993  scmatscmid  31011  mat1dimelbas  31021  dmatelnd  31029  dmatmul  31030  lindslinindimp2lem4  31102  lindslinindsimp2  31104  lindsrng01  31109  snlindsntor  31112  ldepspr  31114  isldepslvec2  31126  rng1nfld  31134  cpmatmcllem  31181  m2pminv2lem  31212  pmatcollpw4fi1lem2  31243  chfacfscmul0  31312  chfacfpmmul0  31316  cayhamlem3  31342  onfrALT  31557  ax6e2ndeq  31568  snssiALT  31864  bnj849  32218  bnj1118  32275  bj-sngltag  32776  bj-bary1lem1  32906  lsatn0  32950  lsatcmp  32954  lssat  32967  lfl1  33021  lshpsmreu  33060  lkrin  33115  glbconxN  33328  cvrat4  33393  paddasslem17  33786  pmodlem2  33797  dalawlem14  33834  pclclN  33841  pclfinN  33850  pclfinclN  33900  poml4N  33903  osumcllem8N  33913  pexmidlem5N  33924  cdleme32a  34391  cdlemg33b0  34651  tendoeq2  34724  diaelrnN  34996  dihmeetlem1N  35241  dihglblem5apreN  35242  dihglblem2N  35245  dochvalr  35308  dochkrshp  35337  lcfl6  35451  lcfrvalsnN  35492  mapdordlem2  35588  mapdh8b  35731  mapdh9a  35741  hdmap14lem13  35834
  Copyright terms: Public domain W3C validator