Theorem eac1i 38

Description: & elimination rule, left hand side. Inference form of ax-eac1 33.

Hypothesis

Ref	Expression
eac1i.1	⊦ (𝜑 & 𝜓)

Assertion

Ref	Expression
eac1i	⊦ 𝜑

Proof of Theorem eac1i

Step	Hyp	Ref	Expression
1		eac1i.1	. . . 4 ⊦ (𝜑 & 𝜓)
2	1	inenebot 27	. . 3 ⊦ (~ ~ ⊥ ⅋ (𝜑 & 𝜓))
3	2	ax-eac1 33	. 2 ⊦ (~ ~ ⊥ ⅋ 𝜑)
4	3	enenebot 28	1 ⊦ 𝜑

Syntax hints:  ⊥wbot 1  ~ wneg 3   & wac 30

This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-init 7  ax-mdco 8  ax-eac1 33

This theorem is referenced by:  etopi  42  lb1d  57  lb2d  58  lbi1s  87  lbi2s  88