Theorem pm3.2i 441

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

Hypotheses

Ref	Expression
pm3.2i.1	⊢ φ
pm3.2i.2	⊢ ψ

Assertion

Ref	Expression
pm3.2i	⊢ (φ ∧ ψ)

Proof of Theorem pm3.2i

Step	Hyp	Ref	Expression
1		pm3.2i.1	. 2 ⊢ φ
2		pm3.2i.2	. 2 ⊢ ψ
3		pm3.2 434	. 2 ⊢ (φ → (ψ → (φ ∧ ψ)))
4	1, 2, 3	mp2 17	1 ⊢ (φ ∧ ψ)

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  3438  ssini  3478  elvvk  4207  ncfinraise  4481  evenoddnnnul  4514  brsi  4761  nfunv  5138  caovcom  5625  mpt2v  5719  op1st2nd  5790  fnfullfun  5858  bren  6030  endisj  6051  ce0addcnnul  6179