Theorem 3pm3.2i 1201

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

Step	Hyp	Ref	Expression
1		3pm3.2i.1	. . 3 |- ph
2		3pm3.2i.2	. . 3 |- ps
3	1, 2	pm3.2i 272	. 2 |- ( ph /\ ps )
4		3pm3.2i.3	. 2 |- ch
5		df-3an 1006	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
6	3, 4, 5	mpbir2an 950	1 |- ( ph /\ ps /\ ch )

Syntax hints:   /\ wa 104   /\ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  mpbir3an  1205  3jaoi  1339  ftp  5838  4bc2eq6  11035  halfleoddlt  12454  strleun  13186  strle1g  13188  slotstnscsi  13277  slotsdnscsi  13305  slotsdifunifndx  13314  2irrexpqap  15701  lgslem2  15729  lgsdir2lem2  15757  lgsdir2lem3  15758  usgrexmpldifpr  16099  0grsubgr  16114  ex-dvds  16326  nconstwlpolem0  16667