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

Theorem syl6bi 231
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
Hypotheses
Ref Expression
syl6bi.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6bi.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6bi  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 210 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 34 1  |-  ( ph  ->  ( ps  ->  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:  ax12i  1785  sb3  2147  2eu2  2350  rgen2aOLD  2851  reu6  3257  sseq0  3791  disjel  3836  disjpss  3840  uneqdifeq  3881  preq12b  4170  prel12  4171  prneimg  4175  elinti  4258  zfrepclf  4536  dtru  4608  opth1g  4690  otsndisj  4718  otiunsndisj  4719  elreldm  5071  issref  5225  relcnvtr  5367  relresfld  5374  ordtr2  5478  nsuceq0  5514  ordssun  5533  ordequn  5534  funopg  5625  funimass2  5667  f0dom0  5776  fveqdmss  6024  eldmrexrnb  6036  fvcofneq  6037  fconstfvOLD  6134  elunirn  6163  oprabid  6324  limuni3  6685  peano5  6722  op1steq  6841  bropopvvv  6879  f1o2ndf1  6907  frxp  6909  fnwelem  6914  suppimacnv  6928  fvn0elsuppb  6935  suppfnss  6943  reldmtpos  6981  rntpos  6986  seqomlem2  7168  oaordi  7247  oa00  7260  oalimcl  7261  omeulem1  7283  nnaordi  7319  ecopovtrn  7466  undifixp  7558  mapdom2  7741  unxpdomlem3  7776  enp1i  7804  findcard2  7809  infssuni  7863  wdompwdom  8091  opthreg  8121  inf3lemd  8130  inf3lem2  8132  inf3lem6  8136  cnfcomlem  8201  cnfcom3  8206  karden  8363  carden2a  8397  alephdom  8508  dfac5lem4  8553  dfac12r  8572  kmlem2  8577  kmlem12  8587  cfslb2n  8694  alephsing  8702  fin23lem30  8768  fin1a2lem6  8831  fin1a2lem13  8838  axcc2lem  8862  domtriomlem  8868  axdc3lem2  8877  axdc4lem  8881  brdom6disj  8956  alephexp1  9000  pwfseq  9085  addnidpi  9322  indpi  9328  nqereu  9350  ltsonq  9390  distrlem5pr  9448  addcanpr  9467  suplem1pr  9473  suplem2pr  9474  ltsrpr  9497  ltsosr  9514  sqgt0sr  9526  leltne  9719  ltnsym  9728  ltlen  9731  eqlei  9740  eqlei2  9741  infm3  10564  nnunb  10861  0mnnnnn0  10898  elnnnn0b  10910  nn0ge2m1nn  10930  btwnz  11033  uz11  11177  zq  11266  xrleltne  11440  xltnegi  11505  xmulasslem2  11564  reltxrnmnf  11628  icogelb  11682  iccleub  11686  uznfz  11871  2ffzeq  11904  elfzonlteqm1  11982  elfznelfzob  12008  injresinjlem  12017  injresinj  12018  fleqceilz  12074  modadd1  12127  modmul1  12136  modirr  12153  uzrdgfni  12165  fsuppmapnn0fiub0  12198  fsuppmapnn0ub  12200  seqf1o  12247  hashrabsn01  12545  hashrabsn1  12546  hash1snb  12584  hashf1lem2  12610  hash2prde  12621  hash2pwpr  12624  hashge2el2dif  12626  hash2sspr  12631  ffz0iswrd  12677  2swrd1eqwrdeq  12791  wrdind  12814  wrd2ind  12815  swrdccatin1  12820  swrdccat3blem  12832  2cshwcshw  12905  cshwcsh2id  12908  wrd2pr2op  13001  2swrd2eqwrdeq  13007  wwlktovf  13010  wwlktovfo  13012  relexpindlem  13105  rexico  13395  lo1le  13693  fsum2dlem  13809  ntrivcvg  13931  fprodss  13980  fprod2dlem  14012  0dvds  14301  gcdneg  14468  algcvga  14516  eucalglt  14522  lcmf  14584  opoe  14739  omoe  14740  opeo  14741  omeo  14742  pockthi  14829  prmreclem5  14842  ramtcl2  14944  ramtcl2OLD  14945  cshwrepswhash1  15051  f1ocpbl  15409  f1ovscpbl  15410  f1olecpbl  15411  monhom  15618  epihom  15625  inveq  15657  invcoisoid  15675  isocoinvid  15676  ciclcl  15685  cicrcl  15686  isinitoi  15876  istermoi  15877  2initoinv  15883  2termoinv  15890  setciso  15964  embedsetcestrclem  16020  ipopos  16384  gsumval2a  16500  ismnddef  16516  symg2bas  17017  symgfix2  17035  gsmsymgreq  17051  pmtrdifellem4  17098  mndodcongi  17170  pj1eu  17324  dprd2da  17653  rimf1o  17940  rimrhm  17941  brric2  17951  lspdisjb  18327  lspsnsubn0  18341  0ring01eq  18473  psrbaglefi  18574  obs2ss  19269  mamufacex  19391  mat0dim0  19469  mat0dimid  19470  mat0dimscm  19471  dmatmat  19496  scmatmat  19511  mat1scmat  19541  1mavmul  19550  mavmulsolcl  19553  gsummatr01  19661  cpmatpmat  19711  cpmadugsumlemF  19877  tg2  19957  unitgOLD  19960  tgcl  19962  neii1  20099  neii2  20101  neindisj2  20116  perfopn  20178  ordtbas2  20184  pnfnei  20213  mnfnei  20214  llyidm  20480  txlm  20640  qtopuni  20694  tgqtop  20704  isfild  20850  snfil  20856  fbunfip  20861  fgss2  20866  fmco  20953  fbflim2  20969  cnpflf2  20992  fcfelbas  21028  fcfneii  21029  alexsubALTlem2  21040  alexsubALT  21043  tgpconcompeqg  21103  tsmscl  21126  tgioo  21791  xrsmopn  21807  iccntr  21816  reconnlem2  21822  addcnlem  21873  htpycn  21981  phtpyhtpy  21990  pi1blem  22047  fgcfil  22218  ioombl1lem4  22491  dyadmbl  22535  itg2gt0  22695  ditgneg  22789  dvivthlem1  22937  coeeq2  23173  aannenlem2  23262  sineq0  23453  efif1o  23472  leibpilem1  23843  xrlimcnp  23871  vmacl  24022  efvmacl  24024  vmalelog  24110  dchrelbasd  24144  lgsqr  24251  uhgra0v  25014  umisuhgra  25031  uslisushgra  25067  uslisumgra  25068  usisuslgra  25069  usgra0v  25075  usgraedgprv  25080  usgra2edg  25086  usgrarnedg  25088  usgraedg4  25091  usgra1v  25094  usgrafisindb0  25112  usgrafisindb1  25113  nbgra0nb  25133  nbcusgra  25167  cusgrasize2inds  25181  cusgrafilem2  25184  usgrasscusgra  25187  uvtxisvtx  25194  2mwlk  25225  wlkcpr  25233  edgwlk  25235  usgrnloop  25269  pthistrl  25278  spthonepeq  25293  wlkdvspthlem  25313  usgra2adedgspthlem2  25316  usgra2adedgwlkonALT  25320  usgra2wlkspthlem1  25323  usgra2wlkspthlem2  25324  usgra2wlkspth  25325  crctistrl  25332  cyclispth  25333  cyclispthon  25337  fargshiftf  25340  fargshiftfo  25342  usgrcyclnl2  25345  3v3e3cycl1  25348  constr3trllem2  25355  4cycl4v4e  25370  4cycl4dv  25371  4cycl4dv4e  25372  wwlknimp  25391  wwlkiswwlkn  25406  2wlkeq  25411  usg2wlkeq  25412  wwlkextproplem3  25447  wwlkextprop  25448  clwwlkprop  25474  clwwlkgt0  25475  clwwlknprop  25476  clwwlknimp  25480  clwlkisclwwlklem2fv2  25487  clwlkisclwwlklem2a4  25488  clwlkisclwwlklem1  25491  clwwlkisclwwlkn  25495  clwwlkext2edg  25506  hashecclwwlkn1  25538  usghashecclwwlk  25539  clwlkf1clwwlklem  25553  el2wlkonotlem  25566  el2wlkonot  25573  el2wlkonotot0  25576  2wlkonot3v  25579  2spthonot3v  25580  el2wlksotot  25586  usg2wlkonot  25587  2spontn0vne  25591  vdgr1a  25610  hashnbgravdg  25617  0eusgraiff0rgracl  25645  rusgrasn  25649  rusgra0edg  25659  clwlknclwlkdifs  25664  frgra3vlem2  25705  1to2vfriswmgra  25710  1to3vfriswmgra  25711  vdfrgra0  25726  vdn0frgrav2  25727  vdgn0frgrav2  25728  frgrancvvdeqlem2  25735  frgrancvvdeqlem4  25737  frgrancvvdeqlemC  25743  usgreghash2spotv  25770  frgregordn0  25774  numclwwlkovf2ex  25790  numclwlk1lem2f1  25798  frgrareggt1  25820  frgrareg  25821  frgraregord013  25822  frgraregord13  25823  clmgmOLD  26025  smgrpmgm  26039  smgrpassOLD  26040  dvrunz  26137  nmlno0lem  26410  normgt0  26756  ocin  26925  nmlnop0iALT  27624  nmopun  27643  cvpss  27914  cvnbtwn  27915  atcvati  28015  mdsymlem6  28037  ifbieq12d2  28139  issgon  28934  mbfmcnt  29079  ballotlemfc0  29314  ballotlemfcc  29315  mthmblem  30207  dfres3  30387  sltsgn1  30536  sltsgn2  30537  sltintdifex  30538  sltres  30539  pprodss4v  30637  funpartfun  30696  funpartfv  30698  5segofs  30759  btwnxfr  30809  brofs2  30830  brifs2  30831  btwnconn1  30854  segleantisym  30868  broutsideof2  30875  outsidene1  30876  outsidene2  30877  funray  30893  lineunray  30900  cldbnd  30968  bj-ax12i  31206  bj-sb3v  31317  bj-dtru  31364  topdifinffinlem  31685  isbasisrelowllem1  31693  isbasisrelowllem2  31694  relowlpssretop  31702  poimir  31881  volsupnfl  31893  itg2addnclem  31901  cover2  31948  sdclem2  31979  fdc  31982  sstotbnd3  32016  heibor1  32050  0rngo  32168  lsatcvat  32529  lshpkrex  32597  cmtbr3N  32733  atn0  32787  atnle  32796  cvlsupr4  32824  cvlsupr5  32825  cvlsupr6  32826  cvrval4N  32892  cvratlem  32899  2llnjN  33045  2lplnj  33098  linepsubN  33230  elpaddatiN  33283  elpcliN  33371  pclcmpatN  33379  ldilval  33591  ltrnu  33599  cdleme18d  33774  tendotp  34241  tendof  34243  tendovalco  34245  diatrl  34525  diaintclN  34539  dvheveccl  34593  dibintclN  34648  dihord6apre  34737  dihmeetlem1N  34771  dihpN  34817  dihintcl  34825  dochkrshp4  34870  pw2f1ocnv  35806  iocinico  36010  expgrowthi  36534  iotavalsb  36636  bi23imp1  36703  ioogtlb  37392  iocgtlb  37399  iocleub  37400  icoltub  37407  iooltub  37410  stoweidlem31  37679  2reu2  38229  eu2ndop1stv  38244  funressnfv  38250  afvelrnb0  38286  el1fzopredsuc  38342  mod2eq1n2dvds  38345  iccpartimp  38351  iccpartrn  38364  iccpartf  38365  iccpartnel  38372  nn0o1gt2ALTV  38443  nn0oALTV  38445  sgoldbaltlem1  38500  nnsum3primesle9  38509  bgoldbtbndlem1  38520  bgoldbtbndlem2  38521  pfxsuff1eqwrdeq  38568  propeqop  38612  iunopeqop  38615  otiunsndisjX  38616  2f1fvneq  38621  funopsn  38625  funsndifnop  38628  fun2dmnop  38632  fzoopth  38659  2ffzoeq  38660  uhgr0v  38721  spthdifv  38728  uhg0v  38751  usgvincvad  38778  usgvincvadALT  38781  usgo0s0  38809  usgo0s0ALT  38810  usgo1s0ALT  38811  usgo1s0  38816  usgfis  38820  usgfisALT  38824  mgmpropd  38837  clcllaw  38889  intop  38901  assintop  38907  assintopcllaw  38910  rngimf1o  38967  rngimrnghm  38968  c0snmgmhm  38976  elrngchom  39032  rnghmsubcsetclem1  39039  rnghmsubcsetclem2  39040  rngcid  39043  rngcinv  39045  rngciso  39046  elrngchomALTV  39050  rngccatidALTV  39053  rngcinvALTV  39057  rngcisoALTV  39058  funcrngcsetcALT  39063  zrinitorngc  39064  zrtermorngc  39065  elringchom  39078  rhmsubcsetclem1  39085  rhmsubcsetclem2  39086  ringcid  39089  rhmsubcrngclem1  39091  rhmsubcrngclem2  39092  ringcinv  39096  ringciso  39097  funcringcsetcALTV2lem7  39106  elringchomALTV  39113  ringccatidALTV  39116  ringcinvALTV  39120  ringcisoALTV  39121  funcringcsetclem7ALTV  39129  irinitoringc  39133  zrtermoringc  39134  rhmsubclem3  39152  rhmsubclem4  39153  rhmsubcALTVlem3  39171  rhmsubcALTVlem4  39172  ztprmneprm  39192  nn0le2is012  39212  suppmptcfin  39228  linccl  39271  linc1  39282  lincolss  39291  ldepspr  39330  nn0o1gt2  39392  nn0sumshdiglem1  39497
  Copyright terms: Public domain W3C validator