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

Theorem syl6bi 220
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 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 31 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  ax11i  1654  equveliOLD  2043  eupickbi  2320  2eu2  2335  rgen2a  2732  reu6  3083  sseq0  3619  disjel  3634  disjpss  3638  uneqdifeq  3676  preq12b  3934  prel12  3935  prneimg  3938  elinti  4019  zfrepclf  4286  dtru  4350  ordtr2  4585  nsuceq0  4621  ordssun  4640  ordequn  4641  limuni3  4791  peano5  4827  elreldm  5053  issref  5206  relcnvtr  5348  relresfld  5355  funopg  5444  funimass2  5486  eldmrexrnb  5836  fconstfv  5913  elunirnALT  5959  oprabid  6064  op1steq  6350  bropopvvv  6385  f1o2ndf1  6413  frxp  6415  fnwelem  6420  reldmtpos  6446  rntpos  6451  seqomlem2  6667  oaordi  6748  oa00  6761  oalimcl  6762  omeulem1  6784  nnaordi  6820  ecopovtrn  6966  undifixp  7057  mapdom2  7237  unxpdomlem3  7274  enp1i  7302  findcard2  7307  wdompwdom  7502  opthreg  7529  inf3lemd  7538  inf3lem2  7540  inf3lem6  7544  karden  7775  carden2a  7809  alephdom  7918  dfac5lem4  7963  dfac12r  7982  kmlem2  7987  kmlem12  7997  cfslb2n  8104  alephsing  8112  fin23lem30  8178  fin1a2lem6  8241  fin1a2lem13  8248  axcc2lem  8272  domtriomlem  8278  axdc3lem2  8287  axdc4lem  8291  brdom6disj  8366  alephexp1  8410  pwfseq  8495  addnidpi  8734  indpi  8740  nqereu  8762  ltsonq  8802  distrlem5pr  8860  addcanpr  8879  suplem1pr  8885  suplem2pr  8886  ltsrpr  8908  ltsosr  8925  sqgt0sr  8937  leltne  9120  ltnsym  9128  ltlen  9131  eqlei  9139  eqlei2  9140  infm3  9923  nnunb  10173  elnnnn0b  10220  btwnz  10328  uz11  10464  zq  10536  xrleltne  10694  xltnegi  10758  xmulasslem2  10817  iccleub  10923  uznfz  11085  elfznelfzob  11148  injresinjlem  11154  injresinj  11155  modadd1  11233  modmul1  11234  modirr  11241  uzrdgfni  11253  seqf1o  11319  hash1snb  11636  hash2prde  11643  hashf1lem2  11660  wrdind  11746  rexico  12112  lo1le  12400  fsum2dlem  12509  0dvds  12825  gcdneg  12981  algcvga  13025  eucalglt  13031  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pockthi  13230  prmreclem5  13243  ramtcl2  13334  f1ocpbl  13705  f1ovscpbl  13706  f1olecpbl  13707  monhom  13916  epihom  13923  setciso  14201  joinlem  14402  meetlem  14409  ipopos  14541  gsumval2a  14737  mndodcongi  15136  pj1eu  15283  dprd2da  15555  lspdisjb  16153  lspsnsubn0  16167  psrbaglefi  16392  obs2ss  16911  tg2  16985  unitg  16987  tgcl  16989  neii1  17125  neii2  17127  neindisj2  17142  perfopn  17203  ordtbas2  17209  pnfnei  17238  mnfnei  17239  llyidm  17504  txlm  17633  qtopuni  17687  tgqtop  17697  isfild  17843  snfil  17849  fbunfip  17854  fgss2  17859  fmco  17946  fbflim2  17962  cnpflf2  17985  fcfelbas  18021  fcfneii  18022  alexsubALTlem2  18032  alexsubALT  18035  tgpconcompeqg  18094  tsmscl  18117  tgioo  18780  xrsmopn  18796  iccntr  18805  reconnlem2  18811  addcnlem  18847  htpycn  18951  phtpyhtpy  18960  pi1blem  19017  fgcfil  19177  ioombl1lem4  19408  dyadmbl  19445  itg2gt0  19605  ditgneg  19697  dvivthlem1  19845  coeeq2  20114  aannenlem2  20199  sineq0  20382  efif1o  20401  leibpilem1  20733  xrlimcnp  20760  vmacl  20854  efvmacl  20856  vmalelog  20942  dchrelbasd  20976  lgsqr  21083  uhgra0v  21298  umisuhgra  21315  uslisumgra  21339  usisuslgra  21340  usgra0v  21344  usgraedgprv  21349  usgra2edg  21355  usgrarnedg  21357  usgraedg4  21359  usgra1v  21362  usgrafisindb0  21375  usgrafisindb1  21376  nbgra0nb  21394  nbcusgra  21425  cusgrasize2inds  21439  cusgrafilem2  21442  usgrasscusgra  21445  uvtxisvtx  21452  2mwlk  21481  usgrnloop  21516  pthistrl  21525  spthonepeq  21540  wlkdvspthlem  21560  crctistrl  21568  cyclispth  21569  cyclispthon  21573  fargshiftf  21576  fargshiftfo  21578  usgrcyclnl2  21581  3v3e3cycl1  21584  constr3trllem2  21591  4cycl4v4e  21606  4cycl4dv  21607  4cycl4dv4e  21608  vdgr1a  21630  hashnbgravdg  21635  clmgm  21862  smgrpmgm  21876  smgrpass  21877  dvrunz  21974  nmlno0lem  22247  normgt0  22582  ocin  22751  nmlnop0iALT  23451  nmopun  23470  cvpss  23741  cvnbtwn  23742  atcvati  23842  mdsymlem6  23864  ifbieq12d2  23955  issgon  24459  mbfmcnt  24571  ballotlemfc0  24703  ballotlemfcc  24704  relexpindlem  25092  ntrivcvg  25178  fprodss  25227  fprod2dlem  25257  dfres3  25330  sltsgn1  25529  sltsgn2  25530  sltintdifex  25531  sltres  25532  pprodss4v  25638  funpartfun  25696  funpartfv  25698  5segofs  25844  btwnxfr  25894  brofs2  25915  brifs2  25916  btwnconn1  25939  segleantisym  25953  broutsideof2  25960  outsidene1  25961  outsidene2  25962  funray  25978  lineunray  25985  volsupnfl  26150  itg2addnclem  26155  cldbnd  26219  cover2  26305  sdclem2  26336  fdc  26339  sstotbnd3  26375  heibor1  26409  0rngo  26527  pw2f1ocnv  26998  expgrowthi  27418  iotavalsb  27501  stoweidlem31  27647  2reu2  27832  eu2ndop1stv  27847  funressnfv  27859  afvelrnb0  27895  otsndisj  27953  otiunsndisj  27954  otiunsndisjX  27955  2f1fvneq  27958  0mnnnnn0  27971  euhash1  27998  iswrd0i  27999  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12  28026  swrdccat3  28029  swrdccat3b  28031  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2wlkspth  28038  spthdifv  28039  usgra2adedgspthlem2  28044  el2wlkonotlem  28059  el2wlkonot  28066  el2wlkonotot0  28069  2wlkonot3v  28072  2spthonot3v  28073  el2wlksotot  28079  usg2wlkonot  28080  2spontn0vne  28084  frgra3vlem2  28105  1to2vfriswmgra  28110  1to3vfriswmgra  28111  vdfrgra0  28126  vdgfrgra0  28127  vdn0frgrav2  28128  vdgn0frgrav2  28129  frgrancvvdeqlem2  28134  frgrancvvdeqlem4  28136  frgrancvvdeqlemC  28142  usgreghash2spotv  28169  frgregordn0  28173  bi23imp1  28292  equveliNEW7  29232  lsatcvat  29533  lshpkrex  29601  cmtbr3N  29737  atn0  29791  atnle  29800  cvlsupr4  29828  cvlsupr5  29829  cvlsupr6  29830  cvrval4N  29896  cvratlem  29903  2llnjN  30049  2lplnj  30102  linepsubN  30234  elpaddatiN  30287  elpcliN  30375  pclcmpatN  30383  ldilval  30595  ltrnu  30603  cdleme18d  30777  tendotp  31243  tendof  31245  tendovalco  31247  diatrl  31527  diaintclN  31541  dvheveccl  31595  dibintclN  31650  dihord6apre  31739  dihmeetlem1N  31773  dihpN  31819  dihintcl  31827  dochkrshp4  31872
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator