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  1710  sb3  2069  eupickbiOLD  2369  2eu2  2388  rgen2aOLD  2892  reu6  3292  sseq0  3817  disjel  3873  disjpss  3877  uneqdifeq  3915  preq12b  4202  prel12  4203  prneimg  4207  elinti  4291  zfrepclf  4564  dtru  4638  opth1g  4723  otsndisj  4752  otiunsndisj  4753  ordtr2  4922  nsuceq0  4958  ordssun  4977  ordequn  4978  elreldm  5227  issref  5380  relcnvtr  5527  relresfld  5534  funopg  5620  funimass2  5662  f0dom0  5769  eldmrexrnb  6028  fvcofneq  6029  fconstfv  6123  elunirn  6151  oprabid  6308  limuni3  6671  peano5  6707  op1steq  6826  bropopvvv  6863  f1o2ndf1  6891  frxp  6893  fnwelem  6898  suppimacnv  6912  suppfnss  6925  reldmtpos  6963  rntpos  6968  seqomlem2  7116  oaordi  7195  oa00  7208  oalimcl  7209  omeulem1  7231  nnaordi  7267  ecopovtrn  7414  undifixp  7505  mapdom2  7688  unxpdomlem3  7726  enp1i  7755  findcard2  7760  infssuni  7811  wdompwdom  8004  opthreg  8035  inf3lemd  8044  inf3lem2  8046  inf3lem6  8050  cnfcomlem  8143  cnfcom3  8148  karden  8313  carden2a  8347  alephdom  8462  dfac5lem4  8507  dfac12r  8526  kmlem2  8531  kmlem12  8541  cfslb2n  8648  alephsing  8656  fin23lem30  8722  fin1a2lem6  8785  fin1a2lem13  8792  axcc2lem  8816  domtriomlem  8822  axdc3lem2  8831  axdc4lem  8835  brdom6disj  8910  alephexp1  8954  pwfseq  9042  addnidpi  9279  indpi  9285  nqereu  9307  ltsonq  9347  distrlem5pr  9405  addcanpr  9424  suplem1pr  9430  suplem2pr  9431  ltsrpr  9454  ltsosr  9471  sqgt0sr  9483  leltne  9674  ltnsym  9683  ltlen  9686  eqlei  9694  eqlei2  9695  infm3  10502  nnunb  10791  0mnnnnn0  10828  elnnnn0b  10840  nn0ge2m1nn  10861  btwnz  10963  uz11  11104  zq  11188  xrleltne  11351  xltnegi  11415  xmulasslem2  11474  iccleub  11580  uznfz  11761  2ffzeq  11791  elfzonlteqm1  11859  elfznelfzob  11884  injresinjlem  11893  injresinj  11894  fleqceilz  11949  modadd1  12001  modmul1  12008  modirr  12025  uzrdgfni  12037  fsuppmapnn0fiub0  12067  fsuppmapnn0ub  12069  seqf1o  12116  hashrabsn01  12409  hashrabsn1  12410  hash1snb  12444  euhash1  12445  hashf1lem2  12471  hash2prde  12482  hash2pwpr  12485  hashge2el2dif  12487  hash2sspr  12492  ffz0iswrd  12534  lswlgt0cl  12555  ccatw2s1p1  12603  swrdvalodm2  12627  2swrd1eqwrdeq  12642  wrdind  12665  wrd2ind  12666  swrdccatin1  12671  swrdccat3blem  12683  2cshwcshw  12756  cshwcsh2id  12759  wrd2pr2op  12848  2swrd2eqwrdeq  12854  wwlktovf  12857  wwlktovfo  12859  rexico  13149  lo1le  13437  fsum2dlem  13548  0dvds  13865  gcdneg  14023  algcvga  14067  eucalglt  14073  opoe  14194  omoe  14195  opeo  14196  omeo  14197  pockthi  14284  prmreclem5  14297  ramtcl2  14388  cshwrepswhash1  14445  f1ocpbl  14780  f1ovscpbl  14781  f1olecpbl  14782  monhom  14991  epihom  14998  setciso  15276  ipopos  15647  gsumval2a  15834  symg2bas  16228  symgfix2  16246  gsmsymgreq  16262  pmtrdifellem4  16310  mndodcongi  16373  pj1eu  16520  dprd2da  16893  rimf1o  17183  rimrhm  17184  brric2  17194  lspdisjb  17572  lspsnsubn0  17586  0rng01eq  17718  psrbaglefi  17822  psrbaglefiOLD  17823  obs2ss  18555  mamufacex  18686  mat0dim0  18764  mat0dimid  18765  mat0dimscm  18766  dmatmat  18791  scmatmat  18806  mat1scmat  18836  1mavmul  18845  mavmulsolcl  18848  gsummatr01  18956  cpmatpmat  19006  cpmadugsumlemF  19172  tg2  19261  unitg  19263  tgcl  19265  neii1  19401  neii2  19403  neindisj2  19418  perfopn  19480  ordtbas2  19486  pnfnei  19515  mnfnei  19516  bwthOLD  19705  llyidm  19783  txlm  19912  qtopuni  19966  tgqtop  19976  isfild  20122  snfil  20128  fbunfip  20133  fgss2  20138  fmco  20225  fbflim2  20241  cnpflf2  20264  fcfelbas  20300  fcfneii  20301  alexsubALTlem2  20311  alexsubALT  20314  tgpconcompeqg  20373  tsmscl  20396  tgioo  21064  xrsmopn  21080  iccntr  21089  reconnlem2  21095  addcnlem  21131  htpycn  21236  phtpyhtpy  21245  pi1blem  21302  fgcfil  21473  ioombl1lem4  21734  dyadmbl  21772  itg2gt0  21930  ditgneg  22024  dvivthlem1  22172  coeeq2  22402  aannenlem2  22487  sineq0  22675  efif1o  22694  leibpilem1  23027  xrlimcnp  23054  vmacl  23148  efvmacl  23150  vmalelog  23236  dchrelbasd  23270  lgsqr  23377  uhgra0v  24014  umisuhgra  24031  uslisushgra  24067  uslisumgra  24068  usisuslgra  24069  usgra0v  24075  usgraedgprv  24080  usgra2edg  24086  usgrarnedg  24088  usgraedg4  24091  usgra1v  24094  usgrafisindb0  24112  usgrafisindb1  24113  nbgra0nb  24133  nbcusgra  24167  cusgrasize2inds  24181  cusgrafilem2  24184  usgrasscusgra  24187  uvtxisvtx  24194  2mwlk  24225  wlkcpr  24233  edgwlk  24235  usgrnloop  24269  pthistrl  24278  spthonepeq  24293  wlkdvspthlem  24313  usgra2adedgspthlem2  24316  usgra2adedgwlkonALT  24320  usgra2wlkspthlem1  24323  usgra2wlkspthlem2  24324  usgra2wlkspth  24325  crctistrl  24332  cyclispth  24333  cyclispthon  24337  fargshiftf  24340  fargshiftfo  24342  usgrcyclnl2  24345  3v3e3cycl1  24348  constr3trllem2  24355  4cycl4v4e  24370  4cycl4dv  24371  4cycl4dv4e  24372  wwlknimp  24391  wwlkiswwlkn  24406  2wlkeq  24411  usg2wlkeq  24412  wwlkextproplem3  24447  wwlkextprop  24448  clwwlkprop  24474  clwwlkgt0  24475  clwwlknprop  24476  clwwlknimp  24480  clwlkisclwwlklem2fv2  24487  clwlkisclwwlklem2a4  24488  clwlkisclwwlklem1  24491  clwwlkisclwwlkn  24495  clwwlkext2edg  24506  hashecclwwlkn1  24538  usghashecclwwlk  24539  el2wlkonotlem  24566  el2wlkonot  24573  el2wlkonotot0  24576  2wlkonot3v  24579  2spthonot3v  24580  el2wlksotot  24586  usg2wlkonot  24587  2spontn0vne  24591  vdgr1a  24610  hashnbgravdg  24617  0eusgraiff0rgracl  24645  rusgrasn  24649  rusgra0edg  24659  clwlknclwlkdifs  24664  frgra3vlem2  24705  1to2vfriswmgra  24710  1to3vfriswmgra  24711  vdfrgra0  24726  vdgfrgra0  24727  vdn0frgrav2  24728  vdgn0frgrav2  24729  frgrancvvdeqlem2  24736  frgrancvvdeqlem4  24738  frgrancvvdeqlemC  24744  usgreghash2spotv  24771  frgregordn0  24775  numclwwlkovf2ex  24791  numclwlk1lem2f1  24799  frgrareggt1  24821  frgrareg  24822  frgraregord013  24823  frgraregord13  24824  clmgm  25027  smgrpmgm  25041  smgrpass  25042  dvrunz  25139  nmlno0lem  25412  normgt0  25748  ocin  25918  nmlnop0iALT  26618  nmopun  26637  cvpss  26908  cvnbtwn  26909  atcvati  27009  mdsymlem6  27031  ifbieq12d2  27122  issgon  27791  mbfmcnt  27907  ballotlemfc0  28099  ballotlemfcc  28100  relexpindlem  28565  ntrivcvg  28636  fprodss  28685  fprod2dlem  28715  dfres3  28793  sltsgn1  29026  sltsgn2  29027  sltintdifex  29028  sltres  29029  pprodss4v  29139  funpartfun  29198  funpartfv  29200  5segofs  29261  btwnxfr  29311  brofs2  29332  brifs2  29333  btwnconn1  29356  segleantisym  29370  broutsideof2  29377  outsidene1  29378  outsidene2  29379  funray  29395  lineunray  29402  volsupnfl  29664  itg2addnclem  29671  cldbnd  29749  cover2  29835  sdclem2  29866  fdc  29869  sstotbnd3  29903  heibor1  29937  0rngo  30055  pw2f1ocnv  30611  iocinico  30812  expgrowthi  30866  iotavalsb  30946  ioogtlb  31120  iocgtlb  31127  iocleub  31128  icogelb  31134  icoltub  31137  iooltub  31140  iblspltprt  31319  stoweidlem31  31359  2reu2  31687  eu2ndop1stv  31702  funressnfv  31708  afvelrnb0  31744  otiunsndisjX  31796  2f1fvneq  31802  fzoopth  31835  2ffzoeq  31836  spthdifv  31847  uhg0v  31872  usgvincvad  31899  usgvincvadALT  31902  usgo0s0  31930  usgo0s0ALT  31931  usgo1s0ALT  31932  usgo1s0  31937  usgfis  31941  usgfisALT  31945  mndmgm  31955  clcllaw  31971  intop  31983  assintop  31989  assintopcllaw  31992  ztprmneprm  32032  nn0le2is012  32053  suppmptcfin  32071  linccl  32114  linc1  32125  lincolss  32134  ldepspr  32173  bi23imp1  32361  bj-ax12i  33333  bj-sb3v  33435  bj-dtru  33482  lsatcvat  33865  lshpkrex  33933  cmtbr3N  34069  atn0  34123  atnle  34132  cvlsupr4  34160  cvlsupr5  34161  cvlsupr6  34162  cvrval4N  34228  cvratlem  34235  2llnjN  34381  2lplnj  34434  linepsubN  34566  elpaddatiN  34619  elpcliN  34707  pclcmpatN  34715  ldilval  34927  ltrnu  34935  cdleme18d  35109  tendotp  35575  tendof  35577  tendovalco  35579  diatrl  35859  diaintclN  35873  dvheveccl  35927  dibintclN  35982  dihord6apre  36071  dihmeetlem1N  36105  dihpN  36151  dihintcl  36159  dochkrshp4  36204
  Copyright terms: Public domain W3C validator