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  1725  sb3  2082  2eu2  2364  rgen2aOLD  2871  reu6  3274  sseq0  3803  disjel  3859  disjpss  3863  uneqdifeq  3902  preq12b  4191  prel12  4192  prneimg  4196  elinti  4280  zfrepclf  4554  dtru  4628  opth1g  4713  otsndisj  4742  otiunsndisj  4743  ordtr2  4912  nsuceq0  4948  ordssun  4967  ordequn  4968  elreldm  5217  issref  5370  relcnvtr  5517  relresfld  5524  funopg  5610  funimass2  5652  f0dom0  5759  fveqdmss  6011  eldmrexrnb  6023  fvcofneq  6024  fconstfvOLD  6119  elunirn  6148  oprabid  6308  limuni3  6672  peano5  6708  op1steq  6827  bropopvvv  6865  f1o2ndf1  6893  frxp  6895  fnwelem  6900  suppimacnv  6914  suppfnss  6927  reldmtpos  6965  rntpos  6970  seqomlem2  7118  oaordi  7197  oa00  7210  oalimcl  7211  omeulem1  7233  nnaordi  7269  ecopovtrn  7416  undifixp  7507  mapdom2  7690  unxpdomlem3  7728  enp1i  7757  findcard2  7762  infssuni  7813  wdompwdom  8007  opthreg  8038  inf3lemd  8047  inf3lem2  8049  inf3lem6  8053  cnfcomlem  8146  cnfcom3  8151  karden  8316  carden2a  8350  alephdom  8465  dfac5lem4  8510  dfac12r  8529  kmlem2  8534  kmlem12  8544  cfslb2n  8651  alephsing  8659  fin23lem30  8725  fin1a2lem6  8788  fin1a2lem13  8795  axcc2lem  8819  domtriomlem  8825  axdc3lem2  8834  axdc4lem  8838  brdom6disj  8913  alephexp1  8957  pwfseq  9045  addnidpi  9282  indpi  9288  nqereu  9310  ltsonq  9350  distrlem5pr  9408  addcanpr  9427  suplem1pr  9433  suplem2pr  9434  ltsrpr  9457  ltsosr  9474  sqgt0sr  9486  leltne  9677  ltnsym  9686  ltlen  9689  eqlei  9697  eqlei2  9698  infm3  10509  nnunb  10798  0mnnnnn0  10835  elnnnn0b  10847  nn0ge2m1nn  10868  btwnz  10972  uz11  11113  zq  11198  xrleltne  11361  xltnegi  11425  xmulasslem2  11484  iccleub  11590  uznfz  11771  2ffzeq  11804  elfzonlteqm1  11872  elfznelfzob  11897  injresinjlem  11906  injresinj  11907  fleqceilz  11962  modadd1  12014  modmul1  12021  modirr  12038  uzrdgfni  12050  fsuppmapnn0fiub0  12080  fsuppmapnn0ub  12082  seqf1o  12129  hashrabsn01  12422  hashrabsn1  12423  hash1snb  12460  hashf1lem2  12486  hash2prde  12497  hash2pwpr  12500  hashge2el2dif  12502  hash2sspr  12507  ffz0iswrd  12549  lswlgt0cl  12571  ccatw2s1p1  12621  swrdvalodm2  12645  2swrd1eqwrdeq  12660  wrdind  12683  wrd2ind  12684  swrdccatin1  12689  swrdccat3blem  12701  2cshwcshw  12774  cshwcsh2id  12777  wrd2pr2op  12866  2swrd2eqwrdeq  12872  wwlktovf  12875  wwlktovfo  12877  rexico  13167  lo1le  13455  fsum2dlem  13566  ntrivcvg  13687  fprodss  13736  fprod2dlem  13765  0dvds  13985  gcdneg  14145  algcvga  14189  eucalglt  14195  opoe  14316  omoe  14317  opeo  14318  omeo  14319  pockthi  14406  prmreclem5  14419  ramtcl2  14510  cshwrepswhash1  14568  f1ocpbl  14903  f1ovscpbl  14904  f1olecpbl  14905  monhom  15111  epihom  15118  setciso  15396  ipopos  15768  gsumval2a  15884  ismnddef  15900  symg2bas  16401  symgfix2  16419  gsmsymgreq  16435  pmtrdifellem4  16482  mndodcongi  16545  pj1eu  16692  dprd2da  17069  rimf1o  17361  rimrhm  17362  brric2  17372  lspdisjb  17750  lspsnsubn0  17764  0ring01eq  17897  psrbaglefi  18001  psrbaglefiOLD  18002  obs2ss  18737  mamufacex  18868  mat0dim0  18946  mat0dimid  18947  mat0dimscm  18948  dmatmat  18973  scmatmat  18988  mat1scmat  19018  1mavmul  19027  mavmulsolcl  19030  gsummatr01  19138  cpmatpmat  19188  cpmadugsumlemF  19354  tg2  19443  unitgOLD  19446  tgcl  19448  neii1  19584  neii2  19586  neindisj2  19601  perfopn  19663  ordtbas2  19669  pnfnei  19698  mnfnei  19699  bwthOLD  19888  llyidm  19966  txlm  20126  qtopuni  20180  tgqtop  20190  isfild  20336  snfil  20342  fbunfip  20347  fgss2  20352  fmco  20439  fbflim2  20455  cnpflf2  20478  fcfelbas  20514  fcfneii  20515  alexsubALTlem2  20525  alexsubALT  20528  tgpconcompeqg  20587  tsmscl  20610  tgioo  21278  xrsmopn  21294  iccntr  21303  reconnlem2  21309  addcnlem  21345  htpycn  21450  phtpyhtpy  21459  pi1blem  21516  fgcfil  21687  ioombl1lem4  21948  dyadmbl  21986  itg2gt0  22144  ditgneg  22238  dvivthlem1  22386  coeeq2  22616  aannenlem2  22701  sineq0  22890  efif1o  22909  leibpilem1  23247  xrlimcnp  23274  vmacl  23368  efvmacl  23370  vmalelog  23456  dchrelbasd  23490  lgsqr  23597  uhgra0v  24286  umisuhgra  24303  uslisushgra  24339  uslisumgra  24340  usisuslgra  24341  usgra0v  24347  usgraedgprv  24352  usgra2edg  24358  usgrarnedg  24360  usgraedg4  24363  usgra1v  24366  usgrafisindb0  24384  usgrafisindb1  24385  nbgra0nb  24405  nbcusgra  24439  cusgrasize2inds  24453  cusgrafilem2  24456  usgrasscusgra  24459  uvtxisvtx  24466  2mwlk  24497  wlkcpr  24505  edgwlk  24507  usgrnloop  24541  pthistrl  24550  spthonepeq  24565  wlkdvspthlem  24585  usgra2adedgspthlem2  24588  usgra2adedgwlkonALT  24592  usgra2wlkspthlem1  24595  usgra2wlkspthlem2  24596  usgra2wlkspth  24597  crctistrl  24604  cyclispth  24605  cyclispthon  24609  fargshiftf  24612  fargshiftfo  24614  usgrcyclnl2  24617  3v3e3cycl1  24620  constr3trllem2  24627  4cycl4v4e  24642  4cycl4dv  24643  4cycl4dv4e  24644  wwlknimp  24663  wwlkiswwlkn  24678  2wlkeq  24683  usg2wlkeq  24684  wwlkextproplem3  24719  wwlkextprop  24720  clwwlkprop  24746  clwwlkgt0  24747  clwwlknprop  24748  clwwlknimp  24752  clwlkisclwwlklem2fv2  24759  clwlkisclwwlklem2a4  24760  clwlkisclwwlklem1  24763  clwwlkisclwwlkn  24767  clwwlkext2edg  24778  hashecclwwlkn1  24810  usghashecclwwlk  24811  el2wlkonotlem  24838  el2wlkonot  24845  el2wlkonotot0  24848  2wlkonot3v  24851  2spthonot3v  24852  el2wlksotot  24858  usg2wlkonot  24859  2spontn0vne  24863  vdgr1a  24882  hashnbgravdg  24889  0eusgraiff0rgracl  24917  rusgrasn  24921  rusgra0edg  24931  clwlknclwlkdifs  24936  frgra3vlem2  24977  1to2vfriswmgra  24982  1to3vfriswmgra  24983  vdfrgra0  24998  vdn0frgrav2  24999  vdgn0frgrav2  25000  frgrancvvdeqlem2  25007  frgrancvvdeqlem4  25009  frgrancvvdeqlemC  25015  usgreghash2spotv  25042  frgregordn0  25046  numclwwlkovf2ex  25062  numclwlk1lem2f1  25070  frgrareggt1  25092  frgrareg  25093  frgraregord013  25094  frgraregord13  25095  clmgmOLD  25299  smgrpmgm  25313  smgrpassOLD  25314  dvrunz  25411  nmlno0lem  25684  normgt0  26020  ocin  26190  nmlnop0iALT  26890  nmopun  26909  cvpss  27180  cvnbtwn  27181  atcvati  27281  mdsymlem6  27303  ifbieq12d2  27396  issgon  28100  mbfmcnt  28216  ballotlemfc0  28408  ballotlemfcc  28409  mthmblem  28917  relexpindlem  29039  dfres3  29163  sltsgn1  29396  sltsgn2  29397  sltintdifex  29398  sltres  29399  pprodss4v  29509  funpartfun  29568  funpartfv  29570  5segofs  29631  btwnxfr  29681  brofs2  29702  brifs2  29703  btwnconn1  29726  segleantisym  29740  broutsideof2  29747  outsidene1  29748  outsidene2  29749  funray  29765  lineunray  29772  volsupnfl  30034  itg2addnclem  30041  cldbnd  30119  cover2  30179  sdclem2  30210  fdc  30213  sstotbnd3  30247  heibor1  30281  0rngo  30399  pw2f1ocnv  30954  iocinico  31155  expgrowthi  31214  iotavalsb  31294  ioogtlb  31464  iocgtlb  31471  iocleub  31472  icogelb  31478  icoltub  31481  iooltub  31484  stoweidlem31  31702  2reu2  32030  eu2ndop1stv  32045  funressnfv  32051  afvelrnb0  32087  otiunsndisjX  32139  2f1fvneq  32145  fzoopth  32178  2ffzoeq  32179  spthdifv  32190  uhg0v  32215  usgvincvad  32242  usgvincvadALT  32245  usgo0s0  32273  usgo0s0ALT  32274  usgo1s0ALT  32275  usgo1s0  32280  usgfis  32284  usgfisALT  32288  mgmpropd  32301  clcllaw  32352  intop  32364  assintop  32370  assintopcllaw  32373  rngimf1o  32429  rngimrnghm  32430  elrngchom  32516  rnghmsubcsetclem1  32523  rnghmsubcsetclem2  32524  rngcid  32527  rngcinv  32529  rngciso  32530  elrngchomOLD  32534  rngccatidOLD  32537  rngcinvOLD  32541  rngcisoOLD  32542  funcrngcsetcALT  32547  elringchom  32559  rhmsubcsetclem1  32566  rhmsubcsetclem2  32567  ringcid  32570  rhmsubcrngclem1  32572  rhmsubcrngclem2  32573  ringcinv  32577  ringciso  32578  funcringcsetcOLD2lem7  32587  elringchomOLD  32594  ringccatidOLD  32597  ringcinvOLD  32601  ringcisoOLD  32602  funcringcsetclem7OLD  32610  rhmsubclem3  32629  rhmsubclem4  32630  rhmsubcOLDlem3  32648  rhmsubcOLDlem4  32649  ztprmneprm  32669  nn0le2is012  32689  suppmptcfin  32707  linccl  32750  linc1  32761  lincolss  32770  ldepspr  32809  bi23imp1  32997  bj-ax12i  33974  bj-sb3v  34084  bj-dtru  34131  lsatcvat  34515  lshpkrex  34583  cmtbr3N  34719  atn0  34773  atnle  34782  cvlsupr4  34810  cvlsupr5  34811  cvlsupr6  34812  cvrval4N  34878  cvratlem  34885  2llnjN  35031  2lplnj  35084  linepsubN  35216  elpaddatiN  35269  elpcliN  35357  pclcmpatN  35365  ldilval  35577  ltrnu  35585  cdleme18d  35760  tendotp  36227  tendof  36229  tendovalco  36231  diatrl  36511  diaintclN  36525  dvheveccl  36579  dibintclN  36634  dihord6apre  36723  dihmeetlem1N  36757  dihpN  36803  dihintcl  36811  dochkrshp4  36856
  Copyright terms: Public domain W3C validator