Theorem eac2i 40

Description: & elimination rule, right hand side. Inference form of ax-eac2 34.

Hypothesis

Ref	Expression
eac2i.1	⊦ (𝜑 & 𝜓)

Assertion

Ref	Expression
eac2i	⊦ 𝜓

Proof of Theorem eac2i

Step	Hyp	Ref	Expression
1		eac2i.1	. . . 4 ⊦ (𝜑 & 𝜓)
2	1	inenebot 27	. . 3 ⊦ (~ ~ ⊥ ⅋ (𝜑 & 𝜓))
3	2	ax-eac2 34	. 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-eac2 34

This theorem is referenced by:  lb2d  58  lbi1s  87  dflb2s  92