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  1699  sb3  2046  eupickbiOLD  2347  2eu2  2366  rgen2a  2803  reu6  3169  sseq0  3690  disjel  3746  disjpss  3750  uneqdifeq  3788  preq12b  4069  prel12  4070  prneimg  4074  elinti  4158  zfrepclf  4430  dtru  4504  opth1g  4589  ordtr2  4784  nsuceq0  4820  ordssun  4839  ordequn  4840  elreldm  5085  issref  5232  relcnvtr  5378  relresfld  5385  funopg  5471  funimass2  5513  f0dom0  5616  eldmrexrnb  5871  fvcofneq  5872  fconstfv  5961  elunirn  5989  oprabid  6136  limuni3  6484  peano5  6520  op1steq  6639  bropopvvv  6674  f1o2ndf1  6701  frxp  6703  fnwelem  6708  suppimacnv  6722  suppfnss  6735  reldmtpos  6774  rntpos  6779  seqomlem2  6927  oaordi  7006  oa00  7019  oalimcl  7020  omeulem1  7042  nnaordi  7078  ecopovtrn  7224  undifixp  7320  mapdom2  7503  unxpdomlem3  7540  enp1i  7568  findcard2  7573  infssuni  7623  wdompwdom  7814  opthreg  7845  inf3lemd  7854  inf3lem2  7856  inf3lem6  7860  cnfcomlem  7953  cnfcom3  7958  karden  8123  carden2a  8157  alephdom  8272  dfac5lem4  8317  dfac12r  8336  kmlem2  8341  kmlem12  8351  cfslb2n  8458  alephsing  8466  fin23lem30  8532  fin1a2lem6  8595  fin1a2lem13  8602  axcc2lem  8626  domtriomlem  8632  axdc3lem2  8641  axdc4lem  8645  brdom6disj  8720  alephexp1  8764  pwfseq  8852  addnidpi  9091  indpi  9097  nqereu  9119  ltsonq  9159  distrlem5pr  9217  addcanpr  9236  suplem1pr  9242  suplem2pr  9243  ltsrpr  9265  ltsosr  9282  sqgt0sr  9294  leltne  9485  ltnsym  9494  ltlen  9497  eqlei  9505  eqlei2  9506  infm3  10310  nnunb  10596  0mnnnnn0  10633  elnnnn0b  10645  btwnz  10765  uz11  10904  zq  10980  xrleltne  11143  xltnegi  11207  xmulasslem2  11266  iccleub  11372  uznfz  11564  elfznelfzob  11652  injresinjlem  11659  injresinj  11660  fleqceilz  11714  modadd1  11766  modmul1  11773  modirr  11790  uzrdgfni  11802  seqf1o  11868  hash1snb  12192  euhash1  12193  hash2prde  12200  hash2pwpr  12203  hashge2el2dif  12205  hashf1lem2  12230  ffz0iswrd  12276  lswlgt0cl  12292  swrdvalodm2  12354  2swrd1eqwrdeq  12369  wrdind  12392  wrd2ind  12393  swrdccatin1  12395  swrdccat3blem  12407  wrd2pr2op  12568  2swrd2eqwrdeq  12574  rexico  12862  lo1le  13150  fsum2dlem  13258  0dvds  13574  gcdneg  13731  algcvga  13775  eucalglt  13781  opoe  13899  omoe  13900  opeo  13901  omeo  13902  pockthi  13989  prmreclem5  14002  ramtcl2  14093  cshwrepswhash1  14150  f1ocpbl  14484  f1ovscpbl  14485  f1olecpbl  14486  monhom  14695  epihom  14702  setciso  14980  ipopos  15351  gsumval2a  15533  symg2bas  15924  symgfix2  15942  gsmsymgreq  15958  pmtrdifellem4  16006  mndodcongi  16067  pj1eu  16214  dprd2da  16563  rimf1o  16845  rimrhm  16846  lspdisjb  17229  lspsnsubn0  17243  psrbaglefi  17463  psrbaglefiOLD  17464  obs2ss  18176  mamufacex  18311  1mavmul  18381  mavmulsolcl  18384  gsummatr01  18487  tg2  18592  unitg  18594  tgcl  18596  neii1  18732  neii2  18734  neindisj2  18749  perfopn  18811  ordtbas2  18817  pnfnei  18846  mnfnei  18847  bwthOLD  19036  llyidm  19114  txlm  19243  qtopuni  19297  tgqtop  19307  isfild  19453  snfil  19459  fbunfip  19464  fgss2  19469  fmco  19556  fbflim2  19572  cnpflf2  19595  fcfelbas  19631  fcfneii  19632  alexsubALTlem2  19642  alexsubALT  19645  tgpconcompeqg  19704  tsmscl  19727  tgioo  20395  xrsmopn  20411  iccntr  20420  reconnlem2  20426  addcnlem  20462  htpycn  20567  phtpyhtpy  20576  pi1blem  20633  fgcfil  20804  ioombl1lem4  21064  dyadmbl  21102  itg2gt0  21260  ditgneg  21354  dvivthlem1  21502  coeeq2  21732  aannenlem2  21817  sineq0  22005  efif1o  22024  leibpilem1  22357  xrlimcnp  22384  vmacl  22478  efvmacl  22480  vmalelog  22566  dchrelbasd  22600  lgsqr  22707  uhgra0v  23266  umisuhgra  23283  uslisumgra  23307  usisuslgra  23308  usgra0v  23312  usgraedgprv  23317  usgra2edg  23323  usgrarnedg  23325  usgraedg4  23327  usgra1v  23330  usgrafisindb0  23343  usgrafisindb1  23344  nbgra0nb  23362  nbcusgra  23393  cusgrasize2inds  23407  cusgrafilem2  23410  usgrasscusgra  23413  uvtxisvtx  23420  2mwlk  23449  usgrnloop  23484  pthistrl  23493  spthonepeq  23508  wlkdvspthlem  23528  crctistrl  23536  cyclispth  23537  cyclispthon  23541  fargshiftf  23544  fargshiftfo  23546  usgrcyclnl2  23549  3v3e3cycl1  23552  constr3trllem2  23559  4cycl4v4e  23574  4cycl4dv  23575  4cycl4dv4e  23576  vdgr1a  23598  hashnbgravdg  23603  clmgm  23830  smgrpmgm  23844  smgrpass  23845  dvrunz  23942  nmlno0lem  24215  normgt0  24551  ocin  24721  nmlnop0iALT  25421  nmopun  25440  cvpss  25711  cvnbtwn  25712  atcvati  25812  mdsymlem6  25834  ifbieq12d2  25925  issgon  26588  mbfmcnt  26705  ballotlemfc0  26897  ballotlemfcc  26898  relexpindlem  27363  ntrivcvg  27434  fprodss  27483  fprod2dlem  27513  dfres3  27591  sltsgn1  27824  sltsgn2  27825  sltintdifex  27826  sltres  27827  pprodss4v  27937  funpartfun  27996  funpartfv  27998  5segofs  28059  btwnxfr  28109  brofs2  28130  brifs2  28131  btwnconn1  28154  segleantisym  28168  broutsideof2  28175  outsidene1  28176  outsidene2  28177  funray  28193  lineunray  28200  volsupnfl  28462  itg2addnclem  28469  cldbnd  28547  cover2  28633  sdclem2  28664  fdc  28667  sstotbnd3  28701  heibor1  28735  0rngo  28853  pw2f1ocnv  29412  iocinico  29613  expgrowthi  29633  iotavalsb  29713  stoweidlem31  29852  2reu2  30037  eu2ndop1stv  30052  funressnfv  30060  afvelrnb0  30096  otsndisj  30157  otiunsndisj  30158  otiunsndisjX  30159  2f1fvneq  30169  2ffzeq  30230  fzoopth  30239  2ffzoeq  30240  elfzonlteqm1  30251  hash2sspr  30253  hashrabsn01  30258  hashrabsn1  30259  wwlktovf  30277  wwlktovfo  30279  ccatw2s1p1  30295  2wlkeq  30314  usg2wlkeq  30315  wlkcpr  30316  edgwlk  30320  usgra2wlkspthlem1  30322  usgra2wlkspthlem2  30323  usgra2wlkspth  30324  spthdifv  30325  usgra2adedgspthlem2  30330  wwlknimp  30347  wwlkiswwlkn  30362  el2wlkonotlem  30407  el2wlkonot  30414  el2wlkonotot0  30417  2wlkonot3v  30420  2spthonot3v  30421  el2wlksotot  30427  usg2wlkonot  30428  2spontn0vne  30432  clwwlkprop  30459  clwwlkgt0  30460  clwwlknprop  30461  clwwlknimp  30465  clwlkisclwwlklem2fv2  30471  clwlkisclwwlklem2a4  30472  clwlkisclwwlklem1  30475  clwwlkisclwwlkn  30479  clwwlkext2edg  30490  erclwwlktr0  30505  cshwlemma1  30515  hashecclwwlkn1  30534  usghashecclwwlk  30535  rusgrasn  30583  wwlkextproplem3  30588  wwlkextprop  30589  rusgra0edg  30599  clwlknclwlkdifs  30604  frgra3vlem2  30619  1to2vfriswmgra  30624  1to3vfriswmgra  30625  vdfrgra0  30640  vdgfrgra0  30641  vdn0frgrav2  30642  vdgn0frgrav2  30643  frgrancvvdeqlem2  30650  frgrancvvdeqlem4  30652  frgrancvvdeqlemC  30658  usgreghash2spotv  30685  frgregordn0  30689  numclwwlkovf2ex  30705  numclwlk1lem2f1  30713  frgrareggt1  30735  frgrareg  30736  frgraregord013  30737  frgraregord13  30738  ztprmneprm  30768  nn0le2is012  30796  0rng01eq  30806  suppmptcfin  30823  fsuppmapnn0ub  30826  fsuppmapnn0fiub0  30831  mat0dim0  30902  mat0dimid  30903  mat0dimscm  30904  scmatmulcl  30925  linccl  30945  linc1  30956  lincolss  30965  ldepspr  31004  cnstpmatpmat  31062  bi23imp1  31295  bj-ax12i  32265  bj-sb3v  32367  bj-dtru  32414  lsatcvat  32791  lshpkrex  32859  cmtbr3N  32995  atn0  33049  atnle  33058  cvlsupr4  33086  cvlsupr5  33087  cvlsupr6  33088  cvrval4N  33154  cvratlem  33161  2llnjN  33307  2lplnj  33360  linepsubN  33492  elpaddatiN  33545  elpcliN  33633  pclcmpatN  33641  ldilval  33853  ltrnu  33861  cdleme18d  34035  tendotp  34501  tendof  34503  tendovalco  34505  diatrl  34785  diaintclN  34799  dvheveccl  34853  dibintclN  34908  dihord6apre  34997  dihmeetlem1N  35031  dihpN  35077  dihintcl  35085  dochkrshp4  35130
  Copyright terms: Public domain W3C validator