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

Theorem syl6bi 220
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 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 31 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  ax11i  1657  equveliOLD  2086  eupickbi  2347  2eu2  2362  rgen2a  2772  reu6  3123  sseq0  3659  disjel  3674  disjpss  3678  uneqdifeq  3716  preq12b  3974  prel12  3975  prneimg  3978  elinti  4059  zfrepclf  4326  dtru  4390  ordtr2  4625  nsuceq0  4661  ordssun  4681  ordequn  4682  limuni3  4832  peano5  4868  elreldm  5094  issref  5247  relcnvtr  5389  relresfld  5396  funopg  5485  funimass2  5527  eldmrexrnb  5877  fconstfv  5954  elunirnALT  6000  oprabid  6105  op1steq  6391  bropopvvv  6426  f1o2ndf1  6454  frxp  6456  fnwelem  6461  reldmtpos  6487  rntpos  6492  seqomlem2  6708  oaordi  6789  oa00  6802  oalimcl  6803  omeulem1  6825  nnaordi  6861  ecopovtrn  7007  undifixp  7098  mapdom2  7278  unxpdomlem3  7315  enp1i  7343  findcard2  7348  infssuni  7397  wdompwdom  7546  opthreg  7573  inf3lemd  7582  inf3lem2  7584  inf3lem6  7588  karden  7819  carden2a  7853  alephdom  7962  dfac5lem4  8007  dfac12r  8026  kmlem2  8031  kmlem12  8041  cfslb2n  8148  alephsing  8156  fin23lem30  8222  fin1a2lem6  8285  fin1a2lem13  8292  axcc2lem  8316  domtriomlem  8322  axdc3lem2  8331  axdc4lem  8335  brdom6disj  8410  alephexp1  8454  pwfseq  8539  addnidpi  8778  indpi  8784  nqereu  8806  ltsonq  8846  distrlem5pr  8904  addcanpr  8923  suplem1pr  8929  suplem2pr  8930  ltsrpr  8952  ltsosr  8969  sqgt0sr  8981  leltne  9164  ltnsym  9172  ltlen  9175  eqlei  9183  eqlei2  9184  infm3  9967  nnunb  10217  elnnnn0b  10264  btwnz  10372  uz11  10508  zq  10580  xrleltne  10738  xltnegi  10802  xmulasslem2  10861  iccleub  10967  uznfz  11130  elfznelfzob  11193  injresinjlem  11199  injresinj  11200  modadd1  11278  modmul1  11279  modirr  11286  uzrdgfni  11298  seqf1o  11364  hash1snb  11681  hash2prde  11688  hashf1lem2  11705  wrdind  11791  rexico  12157  lo1le  12445  fsum2dlem  12554  0dvds  12870  gcdneg  13026  algcvga  13070  eucalglt  13076  opoe  13185  omoe  13186  opeo  13187  omeo  13188  pockthi  13275  prmreclem5  13288  ramtcl2  13379  f1ocpbl  13750  f1ovscpbl  13751  f1olecpbl  13752  monhom  13961  epihom  13968  setciso  14246  joinlem  14447  meetlem  14454  ipopos  14586  gsumval2a  14782  mndodcongi  15181  pj1eu  15328  dprd2da  15600  lspdisjb  16198  lspsnsubn0  16212  psrbaglefi  16437  obs2ss  16956  tg2  17030  unitg  17032  tgcl  17034  neii1  17170  neii2  17172  neindisj2  17187  perfopn  17249  ordtbas2  17255  pnfnei  17284  mnfnei  17285  bwth  17473  llyidm  17551  txlm  17680  qtopuni  17734  tgqtop  17744  isfild  17890  snfil  17896  fbunfip  17901  fgss2  17906  fmco  17993  fbflim2  18009  cnpflf2  18032  fcfelbas  18068  fcfneii  18069  alexsubALTlem2  18079  alexsubALT  18082  tgpconcompeqg  18141  tsmscl  18164  tgioo  18827  xrsmopn  18843  iccntr  18852  reconnlem2  18858  addcnlem  18894  htpycn  18998  phtpyhtpy  19007  pi1blem  19064  fgcfil  19224  ioombl1lem4  19455  dyadmbl  19492  itg2gt0  19652  ditgneg  19744  dvivthlem1  19892  coeeq2  20161  aannenlem2  20246  sineq0  20429  efif1o  20448  leibpilem1  20780  xrlimcnp  20807  vmacl  20901  efvmacl  20903  vmalelog  20989  dchrelbasd  21023  lgsqr  21130  uhgra0v  21345  umisuhgra  21362  uslisumgra  21386  usisuslgra  21387  usgra0v  21391  usgraedgprv  21396  usgra2edg  21402  usgrarnedg  21404  usgraedg4  21406  usgra1v  21409  usgrafisindb0  21422  usgrafisindb1  21423  nbgra0nb  21441  nbcusgra  21472  cusgrasize2inds  21486  cusgrafilem2  21489  usgrasscusgra  21492  uvtxisvtx  21499  2mwlk  21528  usgrnloop  21563  pthistrl  21572  spthonepeq  21587  wlkdvspthlem  21607  crctistrl  21615  cyclispth  21616  cyclispthon  21620  fargshiftf  21623  fargshiftfo  21625  usgrcyclnl2  21628  3v3e3cycl1  21631  constr3trllem2  21638  4cycl4v4e  21653  4cycl4dv  21654  4cycl4dv4e  21655  vdgr1a  21677  hashnbgravdg  21682  clmgm  21909  smgrpmgm  21923  smgrpass  21924  dvrunz  22021  nmlno0lem  22294  normgt0  22629  ocin  22798  nmlnop0iALT  23498  nmopun  23517  cvpss  23788  cvnbtwn  23789  atcvati  23889  mdsymlem6  23911  ifbieq12d2  24002  issgon  24506  mbfmcnt  24618  ballotlemfc0  24750  ballotlemfcc  24751  relexpindlem  25139  ntrivcvg  25225  fprodss  25274  fprod2dlem  25304  dfres3  25382  sltsgn1  25616  sltsgn2  25617  sltintdifex  25618  sltres  25619  pprodss4v  25729  funpartfun  25788  funpartfv  25790  5segofs  25940  btwnxfr  25990  brofs2  26011  brifs2  26012  btwnconn1  26035  segleantisym  26049  broutsideof2  26056  outsidene1  26057  outsidene2  26058  funray  26074  lineunray  26081  volsupnfl  26251  itg2addnclem  26256  cldbnd  26329  cover2  26415  sdclem2  26446  fdc  26449  sstotbnd3  26485  heibor1  26519  0rngo  26637  pw2f1ocnv  27108  expgrowthi  27527  iotavalsb  27610  stoweidlem31  27756  2reu2  27941  eu2ndop1stv  27956  funressnfv  27968  afvelrnb0  28004  otsndisj  28065  otiunsndisj  28066  otiunsndisjX  28067  2f1fvneq  28077  0mnnnnn0  28095  2ffzeq  28121  fzoopth  28139  2ffzoeq  28140  euhash1  28167  iswrd0i  28169  swrdvalodm2  28188  swrdccatin1  28205  swrdccat3blem  28218  cshwssizelem2  28281  2wlkeq  28303  usg2wlkeq  28304  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usgra2wlkspth  28308  spthdifv  28309  usgra2adedgspthlem2  28314  el2wlkonotlem  28329  el2wlkonot  28336  el2wlkonotot0  28339  2wlkonot3v  28342  2spthonot3v  28343  el2wlksotot  28349  usg2wlkonot  28350  2spontn0vne  28354  frgra3vlem2  28391  1to2vfriswmgra  28396  1to3vfriswmgra  28397  vdfrgra0  28412  vdgfrgra0  28413  vdn0frgrav2  28414  vdgn0frgrav2  28415  frgrancvvdeqlem2  28420  frgrancvvdeqlem4  28422  frgrancvvdeqlemC  28428  usgreghash2spotv  28455  frgregordn0  28459  bi23imp1  28578  equveliNEW7  29528  lsatcvat  29848  lshpkrex  29916  cmtbr3N  30052  atn0  30106  atnle  30115  cvlsupr4  30143  cvlsupr5  30144  cvlsupr6  30145  cvrval4N  30211  cvratlem  30218  2llnjN  30364  2lplnj  30417  linepsubN  30549  elpaddatiN  30602  elpcliN  30690  pclcmpatN  30698  ldilval  30910  ltrnu  30918  cdleme18d  31092  tendotp  31558  tendof  31560  tendovalco  31562  diatrl  31842  diaintclN  31856  dvheveccl  31910  dibintclN  31965  dihord6apre  32054  dihmeetlem1N  32088  dihpN  32134  dihintcl  32142  dochkrshp4  32187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator