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

Theorem syl6bi 228
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 207 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  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:  ax12i  1698  sb3  2045  eupickbiOLD  2343  2eu2  2359  rgen2a  2772  reu6  3137  sseq0  3657  disjel  3713  disjpss  3717  uneqdifeq  3755  preq12b  4036  prel12  4037  prneimg  4041  elinti  4125  zfrepclf  4397  dtru  4471  opth1g  4556  ordtr2  4750  nsuceq0  4786  ordssun  4805  ordequn  4806  elreldm  5051  issref  5199  relcnvtr  5345  relresfld  5352  funopg  5438  funimass2  5480  f0dom0  5583  eldmrexrnb  5838  fvcofneq  5839  fconstfv  5927  elunirnALT  5957  oprabid  6104  limuni3  6452  peano5  6488  op1steq  6607  bropopvvv  6642  f1o2ndf1  6669  frxp  6671  fnwelem  6676  suppimacnv  6690  suppfnss  6703  reldmtpos  6742  rntpos  6747  seqomlem2  6892  oaordi  6973  oa00  6986  oalimcl  6987  omeulem1  7009  nnaordi  7045  ecopovtrn  7191  undifixp  7287  mapdom2  7470  unxpdomlem3  7507  enp1i  7535  findcard2  7540  infssuni  7590  wdompwdom  7781  opthreg  7812  inf3lemd  7821  inf3lem2  7823  inf3lem6  7827  cnfcomlem  7920  cnfcom3  7925  karden  8090  carden2a  8124  alephdom  8239  dfac5lem4  8284  dfac12r  8303  kmlem2  8308  kmlem12  8318  cfslb2n  8425  alephsing  8433  fin23lem30  8499  fin1a2lem6  8562  fin1a2lem13  8569  axcc2lem  8593  domtriomlem  8599  axdc3lem2  8608  axdc4lem  8612  brdom6disj  8687  alephexp1  8731  pwfseq  8818  addnidpi  9057  indpi  9063  nqereu  9085  ltsonq  9125  distrlem5pr  9183  addcanpr  9202  suplem1pr  9208  suplem2pr  9209  ltsrpr  9231  ltsosr  9248  sqgt0sr  9260  leltne  9451  ltnsym  9460  ltlen  9463  eqlei  9471  eqlei2  9472  infm3  10276  nnunb  10562  0mnnnnn0  10599  elnnnn0b  10611  btwnz  10731  uz11  10870  zq  10946  xrleltne  11109  xltnegi  11173  xmulasslem2  11232  iccleub  11338  uznfz  11526  elfznelfzob  11614  injresinjlem  11621  injresinj  11622  fleqceilz  11676  modadd1  11728  modmul1  11735  modirr  11752  uzrdgfni  11764  seqf1o  11830  hash1snb  12154  euhash1  12155  hash2prde  12162  hash2pwpr  12165  hashge2el2dif  12167  hashf1lem2  12192  ffz0iswrd  12238  lswlgt0cl  12254  swrdvalodm2  12316  2swrd1eqwrdeq  12331  wrdind  12354  wrd2ind  12355  swrdccatin1  12357  swrdccat3blem  12369  wrd2pr2op  12530  2swrd2eqwrdeq  12536  rexico  12824  lo1le  13112  fsum2dlem  13220  0dvds  13535  gcdneg  13692  algcvga  13736  eucalglt  13742  opoe  13860  omoe  13861  opeo  13862  omeo  13863  pockthi  13950  prmreclem5  13963  ramtcl2  14054  cshwrepswhash1  14111  f1ocpbl  14445  f1ovscpbl  14446  f1olecpbl  14447  monhom  14656  epihom  14663  setciso  14941  ipopos  15312  gsumval2a  15491  symg2bas  15882  symgfix2  15900  gsmsymgreq  15916  pmtrdifellem4  15964  mndodcongi  16025  pj1eu  16172  dprd2da  16514  lspdisjb  17128  lspsnsubn0  17142  psrbaglefi  17374  psrbaglefiOLD  17375  obs2ss  17995  mamufacex  18130  1mavmul  18200  mavmulsolcl  18203  gsummatr01  18306  tg2  18411  unitg  18413  tgcl  18415  neii1  18551  neii2  18553  neindisj2  18568  perfopn  18630  ordtbas2  18636  pnfnei  18665  mnfnei  18666  bwthOLD  18855  llyidm  18933  txlm  19062  qtopuni  19116  tgqtop  19126  isfild  19272  snfil  19278  fbunfip  19283  fgss2  19288  fmco  19375  fbflim2  19391  cnpflf2  19414  fcfelbas  19450  fcfneii  19451  alexsubALTlem2  19461  alexsubALT  19464  tgpconcompeqg  19523  tsmscl  19546  tgioo  20214  xrsmopn  20230  iccntr  20239  reconnlem2  20245  addcnlem  20281  htpycn  20386  phtpyhtpy  20395  pi1blem  20452  fgcfil  20623  ioombl1lem4  20883  dyadmbl  20921  itg2gt0  21079  ditgneg  21173  dvivthlem1  21321  coeeq2  21594  aannenlem2  21679  sineq0  21867  efif1o  21886  leibpilem1  22219  xrlimcnp  22246  vmacl  22340  efvmacl  22342  vmalelog  22428  dchrelbasd  22462  lgsqr  22569  uhgra0v  23066  umisuhgra  23083  uslisumgra  23107  usisuslgra  23108  usgra0v  23112  usgraedgprv  23117  usgra2edg  23123  usgrarnedg  23125  usgraedg4  23127  usgra1v  23130  usgrafisindb0  23143  usgrafisindb1  23144  nbgra0nb  23162  nbcusgra  23193  cusgrasize2inds  23207  cusgrafilem2  23210  usgrasscusgra  23213  uvtxisvtx  23220  2mwlk  23249  usgrnloop  23284  pthistrl  23293  spthonepeq  23308  wlkdvspthlem  23328  crctistrl  23336  cyclispth  23337  cyclispthon  23341  fargshiftf  23344  fargshiftfo  23346  usgrcyclnl2  23349  3v3e3cycl1  23352  constr3trllem2  23359  4cycl4v4e  23374  4cycl4dv  23375  4cycl4dv4e  23376  vdgr1a  23398  hashnbgravdg  23403  clmgm  23630  smgrpmgm  23644  smgrpass  23645  dvrunz  23742  nmlno0lem  24015  normgt0  24351  ocin  24521  nmlnop0iALT  25221  nmopun  25240  cvpss  25511  cvnbtwn  25512  atcvati  25612  mdsymlem6  25634  ifbieq12d2  25726  issgon  26419  mbfmcnt  26536  ballotlemfc0  26722  ballotlemfcc  26723  relexpindlem  27187  ntrivcvg  27258  fprodss  27307  fprod2dlem  27337  dfres3  27415  sltsgn1  27648  sltsgn2  27649  sltintdifex  27650  sltres  27651  pprodss4v  27761  funpartfun  27820  funpartfv  27822  5segofs  27883  btwnxfr  27933  brofs2  27954  brifs2  27955  btwnconn1  27978  segleantisym  27992  broutsideof2  27999  outsidene1  28000  outsidene2  28001  funray  28017  lineunray  28024  volsupnfl  28277  itg2addnclem  28284  cldbnd  28362  cover2  28448  sdclem2  28479  fdc  28482  sstotbnd3  28516  heibor1  28550  0rngo  28668  pw2f1ocnv  29228  iocinico  29429  areaquad  29434  expgrowthi  29449  iotavalsb  29529  stoweidlem31  29669  2reu2  29854  eu2ndop1stv  29869  funressnfv  29877  afvelrnb0  29913  otsndisj  29974  otiunsndisj  29975  otiunsndisjX  29976  2f1fvneq  29986  2ffzeq  30047  fzoopth  30056  2ffzoeq  30057  elfzonlteqm1  30068  hash2sspr  30070  hashrabsn01  30075  hashrabsn1  30076  wwlktovf  30094  wwlktovfo  30096  ccatw2s1p1  30112  2wlkeq  30131  usg2wlkeq  30132  wlkcpr  30133  edgwlk  30137  usgra2wlkspthlem1  30139  usgra2wlkspthlem2  30140  usgra2wlkspth  30141  spthdifv  30142  usgra2adedgspthlem2  30147  wwlknimp  30164  wwlkiswwlkn  30179  el2wlkonotlem  30224  el2wlkonot  30231  el2wlkonotot0  30234  2wlkonot3v  30237  2spthonot3v  30238  el2wlksotot  30244  usg2wlkonot  30245  2spontn0vne  30249  clwwlkprop  30276  clwwlkgt0  30277  clwwlknprop  30278  clwwlknimp  30282  clwlkisclwwlklem2fv2  30288  clwlkisclwwlklem2a4  30289  clwlkisclwwlklem1  30292  clwwlkisclwwlkn  30296  clwwlkext2edg  30307  erclwwlktr0  30322  cshwlemma1  30332  hashecclwwlkn1  30351  usghashecclwwlk  30352  rusgrasn  30400  wwlkextproplem3  30405  wwlkextprop  30406  rusgra0edg  30416  clwlknclwlkdifs  30421  frgra3vlem2  30436  1to2vfriswmgra  30441  1to3vfriswmgra  30442  vdfrgra0  30457  vdgfrgra0  30458  vdn0frgrav2  30459  vdgn0frgrav2  30460  frgrancvvdeqlem2  30467  frgrancvvdeqlem4  30469  frgrancvvdeqlemC  30475  usgreghash2spotv  30502  frgregordn0  30506  numclwwlkovf2ex  30522  numclwlk1lem2f1  30530  frgrareggt1  30552  frgrareg  30553  frgraregord013  30554  frgraregord13  30555  ztprmneprm  30580  nn0le2is012  30594  0rng01eq  30604  suppmptcfin  30620  mat0dim0  30640  mat0dimid  30641  mat0dimscm  30642  linccl  30654  linc1  30665  lincolss  30674  ldepspr  30713  bi23imp1  30897  bj-ax12i  31824  bj-sb3v  31898  bj-dtru  31935  lsatcvat  32265  lshpkrex  32333  cmtbr3N  32469  atn0  32523  atnle  32532  cvlsupr4  32560  cvlsupr5  32561  cvlsupr6  32562  cvrval4N  32628  cvratlem  32635  2llnjN  32781  2lplnj  32834  linepsubN  32966  elpaddatiN  33019  elpcliN  33107  pclcmpatN  33115  ldilval  33327  ltrnu  33335  cdleme18d  33509  tendotp  33975  tendof  33977  tendovalco  33979  diatrl  34259  diaintclN  34273  dvheveccl  34327  dibintclN  34382  dihord6apre  34471  dihmeetlem1N  34505  dihpN  34551  dihintcl  34559  dochkrshp4  34604
  Copyright terms: Public domain W3C validator