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  1637  equveli  1941  eupickbi  2222  2eu2  2237  rgen2a  2622  reu6  2967  sseq0  3499  disjel  3514  disjpss  3518  uneqdifeq  3555  preq12b  3804  prel12  3805  elinti  3887  zfrepclf  4153  dtru  4217  ordtr2  4452  nsuceq0  4488  ordssun  4508  ordequn  4509  limuni3  4659  peano5  4695  elreldm  4919  issref  5072  relcnvtr  5208  relresfld  5215  funopg  5302  funimass2  5342  fconstfv  5750  elunirnALT  5795  oprabid  5898  op1steq  6180  frxp  6241  fnwelem  6246  reldmtpos  6258  rntpos  6263  seqomlem2  6479  oaordi  6560  oa00  6573  oalimcl  6574  omeulem1  6596  nnaordi  6632  ecopovtrn  6777  undifixp  6868  mapdom2  7048  unxpdomlem3  7085  enp1i  7109  findcard2  7114  wdompwdom  7308  opthreg  7335  inf3lemd  7344  inf3lem2  7346  inf3lem6  7350  karden  7581  carden2a  7615  alephdom  7724  dfac5lem4  7769  dfac12r  7788  kmlem2  7793  kmlem12  7803  cfslb2n  7910  alephsing  7918  fin23lem30  7984  fin1a2lem6  8047  fin1a2lem13  8054  axcc2lem  8078  domtriomlem  8084  axdc3lem2  8093  axdc4lem  8097  brdom6disj  8173  alephexp1  8217  pwfseq  8302  addnidpi  8541  indpi  8547  nqereu  8569  ltsonq  8609  distrlem5pr  8667  addcanpr  8686  suplem1pr  8692  suplem2pr  8693  ltsrpr  8715  ltsosr  8732  sqgt0sr  8744  leltne  8927  ltnsym  8935  ltlen  8938  infm3  9729  nnunb  9977  elnnnn0b  10024  btwnz  10130  uz11  10266  zq  10338  xrleltne  10495  xltnegi  10559  xmulasslem2  10618  iccleub  10723  uznfz  10881  modadd1  11017  modmul1  11018  modirr  11025  uzrdgfni  11037  seqf1o  11103  hashf1lem2  11410  wrdind  11493  rexico  11853  lo1le  12141  fsum2dlem  12249  0dvds  12565  gcdneg  12721  algcvga  12765  eucalglt  12771  opoe  12880  omoe  12881  opeo  12882  omeo  12883  pockthi  12970  prmreclem5  12983  ramtcl2  13074  f1ocpbl  13443  f1ovscpbl  13444  f1olecpbl  13445  monhom  13654  epihom  13661  setciso  13939  joinlem  14140  meetlem  14147  ipopos  14279  gsumval2a  14475  mndodcongi  14874  pj1eu  15021  dprd2da  15293  lspdisjb  15895  lspsnsubn0  15909  psrbaglefi  16134  obs2ss  16645  tg2  16719  unitg  16721  tgcl  16723  neii1  16859  neii2  16861  neindisj2  16876  perfopn  16931  ordtbas2  16937  pnfnei  16966  mnfnei  16967  llyidm  17230  txlm  17358  qtopuni  17409  tgqtop  17419  isfild  17569  snfil  17575  fbunfip  17580  fgss2  17585  fmco  17672  fbflim2  17688  cnpflf2  17711  fcfelbas  17747  fcfneii  17748  alexsubALTlem2  17758  alexsubALT  17761  tgpconcompeqg  17810  tsmscl  17833  tgioo  18318  xrsmopn  18334  iccntr  18342  reconnlem2  18348  addcnlem  18384  htpycn  18487  phtpyhtpy  18496  pi1blem  18553  fgcfil  18713  ioombl1lem4  18934  dyadmbl  18971  itg2gt0  19131  ditgneg  19223  dvivthlem1  19371  coeeq2  19640  aannenlem2  19725  sineq0  19905  efif1o  19924  leibpilem1  20252  xrlimcnp  20279  vmacl  20372  efvmacl  20374  vmalelog  20460  dchrelbasd  20494  lgsqr  20601  clmgm  21004  smgrpmgm  21018  smgrpass  21019  dvrunz  21116  nmlno0lem  21387  normgt0  21722  ocin  21891  nmlnop0iALT  22591  nmopun  22610  cvpss  22881  cvnbtwn  22882  atcvati  22982  mdsymlem6  23004  ballotlemfc0  23067  ballotlemfcc  23068  ifbieq12d2  23165  issgon  23499  mbfmcnt  23588  vdgr1a  23912  relexpindlem  24051  dfres3  24187  sltsgn1  24386  sltsgn2  24387  sltintdifex  24388  sltres  24389  pprodss4v  24495  funpartfun  24553  funpartfv  24555  5segofs  24701  btwnxfr  24751  brofs2  24772  brifs2  24773  btwnconn1  24796  segleantisym  24810  broutsideof2  24817  outsidene1  24818  outsidene2  24819  funray  24835  lineunray  24842  itg2addnclem  25003  isunscov  25177  prj1b  25182  prj3  25183  ffvelrnb  25234  iccleub2  25238  iccleub3  25239  sssu  25244  prl2  25272  jop  25287  mop  25288  labs1  25291  labs2  25293  preodom2  25329  preoran2  25333  altprs2  25339  int2pre  25340  supwlub  25377  geme2  25378  dfps2  25392  dffprod  25422  iscomb  25437  mndoid  25460  mndoio  25461  mndoass  25462  mgmrddd  25469  rltrooo  25518  svs2  25590  elioo1t3  25605  truni3  25610  unint2t  25621  intopcoaconlem3  25642  intopcoaconb  25643  limfn  25668  limptlimpr2lem1  25677  limptlimpr2lem2  25678  islimrs  25683  islimrs3  25684  bwt2  25695  iintlem1  25713  addcanrg  25770  hdrmp  25809  obsubc2  25953  idsubc  25954  domsubc  25955  codsubc  25956  subctct  25957  morsubc  25958  cmpsubc  25959  propsrc  25971  tartarmap  25991  elcarelcl  26009  fnctartar  26010  fnctartar2  26011  prismorcset2  26021  isgraphmrph2  26027  domcatsetval2  26032  domcatval2  26034  codcatval2  26040  prismorcset3  26041  rocatval2  26063  setiscat  26082  indcls2  26099  clscnc  26113  pfsubkl  26150  pgapspf  26155  pgapspf2  26156  lineval5a  26191  lineval6a  26192  iscol3  26197  isibg1a6  26228  lppotoslem  26246  nbssntrs  26250  pdiveql  26271  cldbnd  26347  cover2  26461  sdclem2  26555  fdc  26558  sstotbnd3  26603  heibor1  26637  0rngo  26755  pw2f1ocnv  27233  expgrowthi  27653  iotavalsb  27736  stoweidlem31  27883  2reu2  28068  eu2ndop1stv  28083  funressnfv  28096  afvelrnb0  28132  prneimg  28183  injresinjlem  28214  injresinj  28215  uslisumgra  28246  usisuslgra  28247  usgra0v  28251  usgraedgprv  28256  usgra1v  28260  nbgra0nb  28278  nbcusgra  28298  uvtxisvtx  28303  2mwlk  28330  trlonprop  28341  usgrnloop  28351  pthistrl  28358  wlkdvspthlem  28365  crctistrl  28373  cyclispth  28374  cyclispthon  28378  fargshiftf  28381  fargshiftfo  28383  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3trllem2  28397  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414  frgra3vlem2  28425  1to2vfriswmgra  28430  1to3vfriswmgra  28431  equveliNEW7  29503  a12lem1  29752  lsatcvat  29862  lshpkrex  29930  cmtbr3N  30066  atn0  30120  atnle  30129  cvlsupr4  30157  cvlsupr5  30158  cvlsupr6  30159  cvrval4N  30225  cvratlem  30232  2llnjN  30378  2lplnj  30431  linepsubN  30563  elpaddatiN  30616  elpcliN  30704  pclcmpatN  30712  ldilval  30924  ltrnu  30932  cdleme18d  31106  tendotp  31572  tendof  31574  tendovalco  31576  diatrl  31856  diaintclN  31870  dvheveccl  31924  dibintclN  31979  dihord6apre  32068  dihmeetlem1N  32102  dihpN  32148  dihintcl  32156  dochkrshp4  32201
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