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

Theorem syl6bi 219
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 198 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 29 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ax11i  1628  equveli  1928  eupickbi  2209  2eu2  2224  rgen2a  2609  reu6  2954  sseq0  3486  disjel  3501  disjpss  3505  uneqdifeq  3542  preq12b  3788  prel12  3789  elinti  3871  zfrepclf  4137  dtru  4201  ordtr2  4436  nsuceq0  4472  ordssun  4492  ordequn  4493  limuni3  4643  peano5  4679  elreldm  4903  issref  5056  relcnvtr  5192  relresfld  5199  funopg  5286  funimass2  5326  fconstfv  5734  elunirnALT  5779  oprabid  5882  op1steq  6164  frxp  6225  fnwelem  6230  reldmtpos  6242  rntpos  6247  seqomlem2  6463  oaordi  6544  oa00  6557  oalimcl  6558  omeulem1  6580  nnaordi  6616  ecopovtrn  6761  undifixp  6852  mapdom2  7032  unxpdomlem3  7069  enp1i  7093  findcard2  7098  wdompwdom  7292  opthreg  7319  inf3lemd  7328  inf3lem2  7330  inf3lem6  7334  karden  7565  carden2a  7599  alephdom  7708  dfac5lem4  7753  dfac12r  7772  kmlem2  7777  kmlem12  7787  cfslb2n  7894  alephsing  7902  fin23lem30  7968  fin1a2lem6  8031  fin1a2lem13  8038  axcc2lem  8062  domtriomlem  8068  axdc3lem2  8077  axdc4lem  8081  brdom6disj  8157  alephexp1  8201  pwfseq  8286  addnidpi  8525  indpi  8531  nqereu  8553  ltsonq  8593  distrlem5pr  8651  addcanpr  8670  suplem1pr  8676  suplem2pr  8677  ltsrpr  8699  ltsosr  8716  sqgt0sr  8728  leltne  8911  ltnsym  8919  ltlen  8922  infm3  9713  nnunb  9961  elnnnn0b  10008  btwnz  10114  uz11  10250  zq  10322  xrleltne  10479  xltnegi  10543  xmulasslem2  10602  iccleub  10707  uznfz  10865  modadd1  11001  modmul1  11002  modirr  11009  uzrdgfni  11021  seqf1o  11087  hashf1lem2  11394  wrdind  11477  rexico  11837  lo1le  12125  fsum2dlem  12233  0dvds  12549  gcdneg  12705  algcvga  12749  eucalglt  12755  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pockthi  12954  prmreclem5  12967  ramtcl2  13058  f1ocpbl  13427  f1ovscpbl  13428  f1olecpbl  13429  monhom  13638  epihom  13645  setciso  13923  joinlem  14124  meetlem  14131  ipopos  14263  gsumval2a  14459  mndodcongi  14858  pj1eu  15005  dprd2da  15277  lspdisjb  15879  lspsnsubn0  15893  psrbaglefi  16118  obs2ss  16629  tg2  16703  unitg  16705  tgcl  16707  neii1  16843  neii2  16845  neindisj2  16860  perfopn  16915  ordtbas2  16921  pnfnei  16950  mnfnei  16951  llyidm  17214  txlm  17342  qtopuni  17393  tgqtop  17403  isfild  17553  snfil  17559  fbunfip  17564  fgss2  17569  fmco  17656  fbflim2  17672  cnpflf2  17695  fcfelbas  17731  fcfneii  17732  alexsubALTlem2  17742  alexsubALT  17745  tgpconcompeqg  17794  tsmscl  17817  tgioo  18302  xrsmopn  18318  iccntr  18326  reconnlem2  18332  addcnlem  18368  htpycn  18471  phtpyhtpy  18480  pi1blem  18537  fgcfil  18697  ioombl1lem4  18918  dyadmbl  18955  itg2gt0  19115  ditgneg  19207  dvivthlem1  19355  coeeq2  19624  aannenlem2  19709  sineq0  19889  efif1o  19908  leibpilem1  20236  xrlimcnp  20263  vmacl  20356  efvmacl  20358  vmalelog  20444  dchrelbasd  20478  lgsqr  20585  clmgm  20988  smgrpmgm  21002  smgrpass  21003  dvrunz  21100  nmlno0lem  21371  normgt0  21706  ocin  21875  nmlnop0iALT  22575  nmopun  22594  cvpss  22865  cvnbtwn  22866  atcvati  22966  mdsymlem6  22988  ballotlemfc0  23051  ballotlemfcc  23052  ifbieq12d2  23149  issgon  23484  mbfmcnt  23573  vdgr1a  23897  relexpindlem  24036  dfres3  24116  sltsgn1  24315  sltsgn2  24316  sltintdifex  24317  sltres  24318  pprodss4v  24424  5segofs  24629  btwnxfr  24679  brofs2  24700  brifs2  24701  btwnconn1  24724  segleantisym  24738  broutsideof2  24745  outsidene1  24746  outsidene2  24747  funray  24763  lineunray  24770  isunscov  25074  prj1b  25079  prj3  25080  ffvelrnb  25131  iccleub2  25135  iccleub3  25136  sssu  25141  prl2  25169  jop  25184  mop  25185  labs1  25188  labs2  25190  preodom2  25226  preoran2  25230  altprs2  25236  int2pre  25237  supwlub  25274  geme2  25275  dfps2  25289  dffprod  25319  iscomb  25334  mndoid  25357  mndoio  25358  mndoass  25359  mgmrddd  25366  rltrooo  25415  svs2  25487  elioo1t3  25502  truni3  25507  unint2t  25518  intopcoaconlem3  25539  intopcoaconb  25540  limfn  25565  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs  25580  islimrs3  25581  bwt2  25592  iintlem1  25610  addcanrg  25667  hdrmp  25706  obsubc2  25850  idsubc  25851  domsubc  25852  codsubc  25853  subctct  25854  morsubc  25855  cmpsubc  25856  propsrc  25868  tartarmap  25888  elcarelcl  25906  fnctartar  25907  fnctartar2  25908  prismorcset2  25918  isgraphmrph2  25924  domcatsetval2  25929  domcatval2  25931  codcatval2  25937  prismorcset3  25938  rocatval2  25960  setiscat  25979  indcls2  25996  clscnc  26010  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  lineval5a  26088  lineval6a  26089  iscol3  26094  isibg1a6  26125  lppotoslem  26143  nbssntrs  26147  pdiveql  26168  cldbnd  26244  cover2  26358  sdclem2  26452  fdc  26455  sstotbnd3  26500  heibor1  26534  0rngo  26652  pw2f1ocnv  27130  expgrowthi  27550  iotavalsb  27633  stoweidlem31  27780  2reu2  27965  funressnfv  27991  afvelrnb0  28026  prneimg  28073  uslisumgra  28112  usisuslgra  28113  usgra0v  28117  usgraedgprv  28122  usgra1v  28126  nbgra0nb  28144  nbcusgra  28159  uvtxisvtx  28162  frgra3vlem2  28179  1to2vfriswmgra  28184  1to3vfriswmgra  28185  a12lem1  29130  lsatcvat  29240  lshpkrex  29308  cmtbr3N  29444  atn0  29498  atnle  29507  cvlsupr4  29535  cvlsupr5  29536  cvlsupr6  29537  cvrval4N  29603  cvratlem  29610  2llnjN  29756  2lplnj  29809  linepsubN  29941  elpaddatiN  29994  elpcliN  30082  pclcmpatN  30090  ldilval  30302  ltrnu  30310  cdleme18d  30484  tendotp  30950  tendof  30952  tendovalco  30954  diatrl  31234  diaintclN  31248  dvheveccl  31302  dibintclN  31357  dihord6apre  31446  dihmeetlem1N  31480  dihpN  31526  dihintcl  31534  dochkrshp4  31579
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 177
  Copyright terms: Public domain W3C validator