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  5839  4bc2eq6  11037  halfleoddlt  12473  strleun  13205  strle1g  13207  slotstnscsi  13296  slotsdnscsi  13324  slotsdifunifndx  13333  2irrexpqap  15721  lgslem2  15749  lgsdir2lem2  15777  lgsdir2lem3  15778  usgrexmpldifpr  16119  0grsubgr  16134  konigsberglem4  16361  konigsberglem5  16362  ex-dvds  16373  nconstwlpolem0  16719