Theorem pm3.2i 441

Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
pm3.2i.1	|- ph
pm3.2i.2	|- ps

Assertion

Ref	Expression
pm3.2i	|- (ph /\ ps)

Proof of Theorem pm3.2i

Step	Hyp	Ref	Expression
1		pm3.2i.1	. 2 |- ph
2		pm3.2i.2	. 2 |- ps
3		pm3.2 434	. 2 |- (ph -> (ps -> (ph /\ ps)))
4	1, 2, 3	mp2 17	1 |- (ph /\ ps)

Syntax hints:   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  pm4.87  567  dfbi  610  mp4an  654  3pm3.2i  1130  pm11.07  2115  unssi  3439  ssini  3479  elvvk  4208  ncfinraise  4482  evenoddnnnul  4515  brsi  4762  nfunv  5139  caovcom  5626  mpt2v  5720  op1st2nd  5791  fnfullfun  5859  bren  6031  endisj  6052  ce0addcnnul  6180