MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3pm3.2i Unicode version

Theorem 3pm3.2i 1130
Description: Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
Hypotheses
Ref Expression
3pm3.2i.1  |-  ph
3pm3.2i.2  |-  ps
3pm3.2i.3  |-  ch
Assertion
Ref Expression
3pm3.2i  |-  ( ph  /\ 
ps  /\  ch )

Proof of Theorem 3pm3.2i
StepHypRef Expression
1 3pm3.2i.1 . . 3  |-  ph
2 3pm3.2i.2 . . 3  |-  ps
31, 2pm3.2i 441 . 2  |-  ( ph  /\ 
ps )
4 3pm3.2i.3 . 2  |-  ch
5 df-3an 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 886 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mpbir3an  1134  3jaoi  1245  hartogslem1  7257  cantnflem3  7393  cantnflem4  7394  trcl  7410  ttukeylem7  8142  faclbnd4lem1  11306  hashmap  11387  infcvgaux1i  12315  strleun  13238  strle1  13239  zfbas  17591  sincos6thpi  19883  1cubr  20138  birthdaylem1  20246  divsqrsumlem  20274  lgslem2  20536  lgsdir2lem2  20563  lgsdir2lem3  20564  ex-dvds  20835  sspid  21301  lnocoi  21335  nmlno0lem  21371  nmblolbii  21377  blocnilem  21382  phpar  21402  ip0i  21403  ip2i  21406  ipdirilem  21407  ipasslem10  21417  ip2dii  21422  siilem1  21429  siilem2  21430  hhsst  21843  hhsssh2  21847  fh1i  22200  fh2i  22201  cm2ji  22204  pjoi0i  22297  elunop2  22593  mdslle1i  22897  mdslle2i  22898  mdslj1i  22899  mdslj2i  22900  mdslmd1lem1  22905  mdslmd2i  22910  ballotlem2  23047  xrge0iifmhm  23321  dmvlsiga  23490  4bc2eq6  24099  axlowdimlem6  24575  eloi  25086  inposet  25278  dispos  25287  glmrngo  25482  1alg  25722  1ded  25738  dedalg  25743  0alg  25756  0ded  25757  0catOLD  25758  1cat  25759  catded  25764  dualalg  25782  catsbc  25849  setiscat  25979  fnckle  26045  pgapspf  26052  rabren3dioph  26898  jm2.23  27089  lhe4.4ex1a  27546  itgsin0pilem1  27744  stoweidlem5  27754  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem26  27775  stoweidlem28  27777  stoweidlem34  27783  stoweidlem59  27808  stoweidlem62  27811  stoweid  27812  wallispilem2  27815  wallispilem4  27817  wallispi  27819  wallispi2lem1  27820  stirlinglem13  27835  usgraexmpldifpr  28132  isopiN  29371  ishlatiN  29545
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  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator