ndoril-P3.10 - bfol.mm Proof Explorer

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

Theorem ndoril-P3.10 175

Description: Natural Deduction: Left '∨' Introduction Rule.

Deduce a new disjunction containing an arbitrary WFF to the left of a previously deduced WFF.

**Hypothesis**
Ref	Expression
ndoril-P3.10.1	⊢ (𝛾 → 𝜑)

**Assertion**
Ref	Expression
ndoril-P3.10	⊢ (𝛾 → (𝜓 ∨ 𝜑))

**Proof of Theorem ndoril-P3.10**
Step	Hyp	Ref	Expression
1		ndoril-P3.10.1	. 2 ⊢ (𝛾 → 𝜑)
2	1	orintl-P2.11a.AC.SH 147	1 ⊢ (𝛾 → (𝜓 ∨ 𝜑))

Colors of variables: wff objvar term class

Syntax hints: → wff-imp 10 ∨ wff-or 144

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-or-D2.3 145