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

Theorem 3pm3.2i 1132
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 442 . 2  |-  ( ph  /\ 
ps )
4 3pm3.2i.3 . 2  |-  ch
5 df-3an 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 887 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mpbir3an  1136  3jaoi  1247  ftp  5876  hartogslem1  7467  cantnflem3  7603  cantnflem4  7604  trcl  7620  ttukeylem7  8351  faclbnd4lem1  11539  hashmap  11653  infcvgaux1i  12591  strleun  13514  strle1  13515  zfbas  17881  ust0  18202  utop2nei  18233  sincos6thpi  20376  1cubr  20635  birthdaylem1  20743  divsqrsumlem  20771  lgslem2  21034  lgsdir2lem2  21061  lgsdir2lem3  21062  usgraexmpldifpr  21372  2trllemH  21505  2trllemD  21510  2trllemG  21511  wlkntrl  21515  constr2spthlem1  21547  constr3lem2  21586  constr3trllem2  21591  ex-dvds  21709  sspid  22177  lnocoi  22211  nmlno0lem  22247  nmblolbii  22253  blocnilem  22258  phpar  22278  ip0i  22279  ip2i  22282  ipdirilem  22283  ipasslem10  22293  ip2dii  22298  siilem1  22305  siilem2  22306  hhsst  22719  hhsssh2  22723  fh1i  23076  fh2i  23077  cm2ji  23080  pjoi0i  23173  elunop2  23469  mdslle1i  23773  mdslle2i  23774  mdslj1i  23775  mdslj2i  23776  mdslmd1lem1  23781  mdslmd2i  23786  xrge0iifmhm  24278  cnzh  24307  rezh  24308  dmvlsiga  24465  ballotlem2  24699  4bc2eq6  25157  axlowdimlem6  25790  rabren3dioph  26766  jm2.23  26957  lhe4.4ex1a  27414  stoweidlem13  27629  stoweidlem26  27642  stoweidlem34  27650  stoweid  27679  wallispilem2  27682  f13idfv  27963  usgra2pthspth  28035  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  isopiN  29664  ishlatiN  29838
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  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator