ndandel-P3.8 - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > ndandel-P3.8

Theorem ndandel-P3.8 173

Description: Natural Deduction: Left '∧' Elimination Rule.

Deduce the right conjunct (i.e. eliminate the left conjunct) of a previously deduced conjunction.

**Hypothesis**
Ref	Expression
ndandel-P3.8.1	⊢ (𝛾 → (𝜑 ∧ 𝜓))

**Assertion**
Ref	Expression
ndandel-P3.8	⊢ (𝛾 → 𝜓)

**Proof of Theorem ndandel-P3.8**
Step	Hyp	Ref	Expression
1		ndandel-P3.8.1	. 2 ⊢ (𝛾 → (𝜑 ∧ 𝜓))
2	1	simpr-P2.9b.AC.SH 137	1 ⊢ (𝛾 → 𝜓)

Colors of variables: wff objvar term class

Syntax hints: → wff-imp 10 ∧ wff-and 132

This theorem was proved from axioms: ax-L1 11 ax-L2 12 ax-L3 13 ax-MP 14

This theorem depends on definitions: df-bi-D2.1 107 df-and-D2.2 133