Axiom ax-ia3 100

Description: 'And' introduction. Axiom 3 of 10 for intuitionistic logic.

Assertion

Ref	Expression
ax-ia3	|- (ph -> (ps -> (ph /\ ps)))

Detailed syntax breakdown of Axiom ax-ia3

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		wps	. . 3 wff ps
3	1, 2	wa 96	. . 3 wff (ph /\ ps)
4	2, 3	wi 4	. 2 wff (ps -> (ph /\ ps))
5	1, 4	wi 4	1 wff (ph -> (ps -> (ph /\ ps)))

This axiom is referenced by:  ex  107