Theorem 3pm3.2i 1206

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 1011	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
6	3, 4, 5	mpbir2an 955	1 |- ( ph /\ ps /\ ch )

This proof depends on syntax axioms:   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mpbir3an  1210  3jaoi  1344  ftp  5903  4bc2eq6  11235  halfleoddlt  12686  ballotfilemonn  13279  strleun  13517  strle1g  13519  slotstnscsi  13608  slotsdnscsi  13636  slotsdifunifndx  13645  2irrexpqap  16214  lgslem2  16325  lgsdir2lem2  16353  lgsdir2lem3  16354  usgrexmpldifpr  16695  0grsubgr  16710  konigsberglem4  16937  konigsberglem5  16938  ex-dvds  16949  nconstwlpolem0  17320