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  7273  cantnflem3  7409  cantnflem4  7410  trcl  7426  ttukeylem7  8158  faclbnd4lem1  11322  hashmap  11403  infcvgaux1i  12331  strleun  13254  strle1  13255  zfbas  17607  sincos6thpi  19899  1cubr  20154  birthdaylem1  20262  divsqrsumlem  20290  lgslem2  20552  lgsdir2lem2  20579  lgsdir2lem3  20580  ex-dvds  20851  sspid  21317  lnocoi  21351  nmlno0lem  21387  nmblolbii  21393  blocnilem  21398  phpar  21418  ip0i  21419  ip2i  21422  ipdirilem  21423  ipasslem10  21433  ip2dii  21438  siilem1  21445  siilem2  21446  hhsst  21859  hhsssh2  21863  fh1i  22216  fh2i  22217  cm2ji  22220  pjoi0i  22313  elunop2  22609  mdslle1i  22913  mdslle2i  22914  mdslj1i  22915  mdslj2i  22916  mdslmd1lem1  22921  mdslmd2i  22926  ballotlem2  23063  xrge0iifmhm  23336  dmvlsiga  23505  4bc2eq6  24114  axlowdimlem6  24647  eloi  25189  inposet  25381  dispos  25390  glmrngo  25585  1alg  25825  1ded  25841  dedalg  25846  0alg  25859  0ded  25860  0catOLD  25861  1cat  25862  catded  25867  dualalg  25885  catsbc  25952  setiscat  26082  fnckle  26148  pgapspf  26155  rabren3dioph  27001  jm2.23  27192  lhe4.4ex1a  27649  itgsin0pilem1  27847  stoweidlem5  27857  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem26  27878  stoweidlem28  27880  stoweidlem34  27886  stoweidlem59  27911  stoweidlem62  27914  stoweid  27915  wallispilem2  27918  wallispilem4  27920  wallispi  27922  wallispi2lem1  27923  stirlinglem13  27938  usgraexmpldifpr  28266  wlkntrl  28350  constr3lem2  28392  constr3trllem2  28397  isopiN  29993  ishlatiN  30167
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