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 31 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  1762  sb3  2120  2eu2  2329  rgen2aOLD  2831  reu6  3237  sseq0  3770  disjel  3815  disjpss  3819  uneqdifeq  3859  preq12b  4147  prel12  4148  prneimg  4152  elinti  4235  zfrepclf  4512  dtru  4584  opth1g  4666  otsndisj  4694  otiunsndisj  4695  elreldm  5047  issref  5200  relcnvtr  5342  relresfld  5349  ordtr2  5453  nsuceq0  5489  ordssun  5508  ordequn  5509  funopg  5600  funimass2  5642  f0dom0  5751  fveqdmss  6003  eldmrexrnb  6015  fvcofneq  6016  fconstfvOLD  6114  elunirn  6143  oprabid  6304  limuni3  6669  peano5  6706  op1steq  6825  bropopvvv  6863  f1o2ndf1  6891  frxp  6893  fnwelem  6898  suppimacnv  6912  fvn0elsuppb  6919  suppfnss  6927  reldmtpos  6965  rntpos  6970  seqomlem2  7152  oaordi  7231  oa00  7244  oalimcl  7245  omeulem1  7267  nnaordi  7303  ecopovtrn  7450  undifixp  7542  mapdom2  7725  unxpdomlem3  7760  enp1i  7788  findcard2  7793  infssuni  7844  wdompwdom  8037  opthreg  8067  inf3lemd  8076  inf3lem2  8078  inf3lem6  8082  cnfcomlem  8174  cnfcom3  8179  karden  8344  carden2a  8378  alephdom  8493  dfac5lem4  8538  dfac12r  8557  kmlem2  8562  kmlem12  8572  cfslb2n  8679  alephsing  8687  fin23lem30  8753  fin1a2lem6  8816  fin1a2lem13  8823  axcc2lem  8847  domtriomlem  8853  axdc3lem2  8862  axdc4lem  8866  brdom6disj  8941  alephexp1  8985  pwfseq  9071  addnidpi  9308  indpi  9314  nqereu  9336  ltsonq  9376  distrlem5pr  9434  addcanpr  9453  suplem1pr  9459  suplem2pr  9460  ltsrpr  9483  ltsosr  9500  sqgt0sr  9512  leltne  9704  ltnsym  9713  ltlen  9716  eqlei  9725  eqlei2  9726  infm3  10541  nnunb  10831  0mnnnnn0  10868  elnnnn0b  10880  nn0ge2m1nn  10901  btwnz  11004  uz11  11148  zq  11232  xrleltne  11403  xltnegi  11467  xmulasslem2  11526  iccleub  11632  uznfz  11814  2ffzeq  11847  elfzonlteqm1  11925  elfznelfzob  11951  injresinjlem  11960  injresinj  11961  fleqceilz  12017  modadd1  12070  modmul1  12079  modirr  12096  uzrdgfni  12108  fsuppmapnn0fiub0  12141  fsuppmapnn0ub  12143  seqf1o  12190  hashrabsn01  12487  hashrabsn1  12488  hash1snb  12526  hashf1lem2  12552  hash2prde  12563  hash2pwpr  12566  hashge2el2dif  12568  hash2sspr  12573  ffz0iswrd  12619  2swrd1eqwrdeq  12733  wrdind  12756  wrd2ind  12757  swrdccatin1  12762  swrdccat3blem  12774  2cshwcshw  12847  cshwcsh2id  12850  wrd2pr2op  12939  2swrd2eqwrdeq  12945  wwlktovf  12948  wwlktovfo  12950  relexpindlem  13043  rexico  13333  lo1le  13621  fsum2dlem  13734  ntrivcvg  13856  fprodss  13905  fprod2dlem  13934  0dvds  14211  gcdneg  14371  algcvga  14415  eucalglt  14421  opoe  14542  omoe  14543  opeo  14544  omeo  14545  pockthi  14632  prmreclem5  14645  ramtcl2  14736  cshwrepswhash1  14794  f1ocpbl  15137  f1ovscpbl  15138  f1olecpbl  15139  monhom  15346  epihom  15353  inveq  15385  invcoisoid  15403  isocoinvid  15404  ciclcl  15413  cicrcl  15414  isinitoi  15604  istermoi  15605  2initoinv  15611  2termoinv  15618  setciso  15692  embedsetcestrclem  15748  ipopos  16112  gsumval2a  16228  ismnddef  16244  symg2bas  16745  symgfix2  16763  gsmsymgreq  16779  pmtrdifellem4  16826  mndodcongi  16889  pj1eu  17036  dprd2da  17409  rimf1o  17701  rimrhm  17702  brric2  17712  lspdisjb  18090  lspsnsubn0  18104  0ring01eq  18237  psrbaglefi  18341  psrbaglefiOLD  18342  obs2ss  19056  mamufacex  19181  mat0dim0  19259  mat0dimid  19260  mat0dimscm  19261  dmatmat  19286  scmatmat  19301  mat1scmat  19331  1mavmul  19340  mavmulsolcl  19343  gsummatr01  19451  cpmatpmat  19501  cpmadugsumlemF  19667  tg2  19756  unitgOLD  19759  tgcl  19761  neii1  19898  neii2  19900  neindisj2  19915  perfopn  19977  ordtbas2  19983  pnfnei  20012  mnfnei  20013  llyidm  20279  txlm  20439  qtopuni  20493  tgqtop  20503  isfild  20649  snfil  20655  fbunfip  20660  fgss2  20665  fmco  20752  fbflim2  20768  cnpflf2  20791  fcfelbas  20827  fcfneii  20828  alexsubALTlem2  20838  alexsubALT  20841  tgpconcompeqg  20900  tsmscl  20923  tgioo  21591  xrsmopn  21607  iccntr  21616  reconnlem2  21622  addcnlem  21658  htpycn  21763  phtpyhtpy  21772  pi1blem  21829  fgcfil  22000  ioombl1lem4  22261  dyadmbl  22299  itg2gt0  22457  ditgneg  22551  dvivthlem1  22699  coeeq2  22929  aannenlem2  23015  sineq0  23204  efif1o  23223  leibpilem1  23594  xrlimcnp  23622  vmacl  23771  efvmacl  23773  vmalelog  23859  dchrelbasd  23893  lgsqr  24000  uhgra0v  24714  umisuhgra  24731  uslisushgra  24767  uslisumgra  24768  usisuslgra  24769  usgra0v  24775  usgraedgprv  24780  usgra2edg  24786  usgrarnedg  24788  usgraedg4  24791  usgra1v  24794  usgrafisindb0  24812  usgrafisindb1  24813  nbgra0nb  24833  nbcusgra  24867  cusgrasize2inds  24881  cusgrafilem2  24884  usgrasscusgra  24887  uvtxisvtx  24894  2mwlk  24925  wlkcpr  24933  edgwlk  24935  usgrnloop  24969  pthistrl  24978  spthonepeq  24993  wlkdvspthlem  25013  usgra2adedgspthlem2  25016  usgra2adedgwlkonALT  25020  usgra2wlkspthlem1  25023  usgra2wlkspthlem2  25024  usgra2wlkspth  25025  crctistrl  25032  cyclispth  25033  cyclispthon  25037  fargshiftf  25040  fargshiftfo  25042  usgrcyclnl2  25045  3v3e3cycl1  25048  constr3trllem2  25055  4cycl4v4e  25070  4cycl4dv  25071  4cycl4dv4e  25072  wwlknimp  25091  wwlkiswwlkn  25106  2wlkeq  25111  usg2wlkeq  25112  wwlkextproplem3  25147  wwlkextprop  25148  clwwlkprop  25174  clwwlkgt0  25175  clwwlknprop  25176  clwwlknimp  25180  clwlkisclwwlklem2fv2  25187  clwlkisclwwlklem2a4  25188  clwlkisclwwlklem1  25191  clwwlkisclwwlkn  25195  clwwlkext2edg  25206  hashecclwwlkn1  25238  usghashecclwwlk  25239  clwlkf1clwwlklem  25253  el2wlkonotlem  25266  el2wlkonot  25273  el2wlkonotot0  25276  2wlkonot3v  25279  2spthonot3v  25280  el2wlksotot  25286  usg2wlkonot  25287  2spontn0vne  25291  vdgr1a  25310  hashnbgravdg  25317  0eusgraiff0rgracl  25345  rusgrasn  25349  rusgra0edg  25359  clwlknclwlkdifs  25364  frgra3vlem2  25405  1to2vfriswmgra  25410  1to3vfriswmgra  25411  vdfrgra0  25426  vdn0frgrav2  25427  vdgn0frgrav2  25428  frgrancvvdeqlem2  25435  frgrancvvdeqlem4  25437  frgrancvvdeqlemC  25443  usgreghash2spotv  25470  frgregordn0  25474  numclwwlkovf2ex  25490  numclwlk1lem2f1  25498  frgrareggt1  25520  frgrareg  25521  frgraregord013  25522  frgraregord13  25523  clmgmOLD  25723  smgrpmgm  25737  smgrpassOLD  25738  dvrunz  25835  nmlno0lem  26108  normgt0  26444  ocin  26614  nmlnop0iALT  27313  nmopun  27332  cvpss  27603  cvnbtwn  27604  atcvati  27704  mdsymlem6  27726  ifbieq12d2  27827  issgon  28557  mbfmcnt  28702  ballotlemfc0  28923  ballotlemfcc  28924  mthmblem  29779  dfres3  29959  sltsgn1  30108  sltsgn2  30109  sltintdifex  30110  sltres  30111  pprodss4v  30209  funpartfun  30268  funpartfv  30270  5segofs  30331  btwnxfr  30381  brofs2  30402  brifs2  30403  btwnconn1  30426  segleantisym  30440  broutsideof2  30447  outsidene1  30448  outsidene2  30449  funray  30465  lineunray  30472  cldbnd  30541  bj-ax12i  30777  bj-sb3v  30887  bj-dtru  30934  topdifinffinlem  31251  isbasisrelowllem1  31259  isbasisrelowllem2  31260  volsupnfl  31411  itg2addnclem  31419  cover2  31466  sdclem2  31497  fdc  31500  sstotbnd3  31534  heibor1  31568  0rngo  31686  lsatcvat  32048  lshpkrex  32116  cmtbr3N  32252  atn0  32306  atnle  32315  cvlsupr4  32343  cvlsupr5  32344  cvlsupr6  32345  cvrval4N  32411  cvratlem  32418  2llnjN  32564  2lplnj  32617  linepsubN  32749  elpaddatiN  32802  elpcliN  32890  pclcmpatN  32898  ldilval  33110  ltrnu  33118  cdleme18d  33293  tendotp  33760  tendof  33762  tendovalco  33764  diatrl  34044  diaintclN  34058  dvheveccl  34112  dibintclN  34167  dihord6apre  34256  dihmeetlem1N  34290  dihpN  34336  dihintcl  34344  dochkrshp4  34389  pw2f1ocnv  35321  iocinico  35523  expgrowthi  36066  iotavalsb  36168  bi23imp1  36261  ioogtlb  36877  iocgtlb  36884  iocleub  36885  icogelb  36891  icoltub  36894  iooltub  36897  stoweidlem31  37162  2reu2  37541  eu2ndop1stv  37556  funressnfv  37562  afvelrnb0  37598  el1fzopredsuc  37654  mod2eq1n2dvds  37657  iccpartimp  37665  iccpartrn  37678  iccpartf  37679  iccpartnel  37686  nn0o1gt2ALTV  37757  nn0oALTV  37759  sgoldbaltlem1  37814  nnsum3primesle9  37823  bgoldbtbndlem1  37834  bgoldbtbndlem2  37835  pfxsuff1eqwrdeq  37875  otiunsndisjX  37915  2f1fvneq  37921  fzoopth  37952  2ffzoeq  37953  spthdifv  37962  uhg0v  37987  usgvincvad  38014  usgvincvadALT  38017  usgo0s0  38045  usgo0s0ALT  38046  usgo1s0ALT  38047  usgo1s0  38052  usgfis  38056  usgfisALT  38060  mgmpropd  38073  clcllaw  38125  intop  38137  assintop  38143  assintopcllaw  38146  rngimf1o  38203  rngimrnghm  38204  c0snmgmhm  38212  elrngchom  38268  rnghmsubcsetclem1  38275  rnghmsubcsetclem2  38276  rngcid  38279  rngcinv  38281  rngciso  38282  elrngchomALTV  38286  rngccatidALTV  38289  rngcinvALTV  38293  rngcisoALTV  38294  funcrngcsetcALT  38299  zrinitorngc  38300  zrtermorngc  38301  elringchom  38314  rhmsubcsetclem1  38321  rhmsubcsetclem2  38322  ringcid  38325  rhmsubcrngclem1  38327  rhmsubcrngclem2  38328  ringcinv  38332  ringciso  38333  funcringcsetcALTV2lem7  38342  elringchomALTV  38349  ringccatidALTV  38352  ringcinvALTV  38356  ringcisoALTV  38357  funcringcsetclem7ALTV  38365  irinitoringc  38369  zrtermoringc  38370  rhmsubclem3  38388  rhmsubclem4  38389  rhmsubcALTVlem3  38407  rhmsubcALTVlem4  38408  ztprmneprm  38428  nn0le2is012  38448  suppmptcfin  38464  linccl  38507  linc1  38518  lincolss  38527  ldepspr  38566  nn0o1gt2  38628  nn0sumshdiglem1  38733
  Copyright terms: Public domain W3C validator