ndimp-P3.2 - bfol.mm Proof Explorer

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

Theorem ndimp-P3.2 167

Description: Natural Deduction: Import Previous Consequent.

Any previous consequent can be re-stated with an additional assumption added.

**Hypothesis**
Ref	Expression
ndimp-P3.2.1	⊢ (𝛾 → 𝜑)

**Assertion**
Ref	Expression
ndimp-P3.2	⊢ ((𝛾 ∧ 𝜓) → 𝜑)

**Proof of Theorem ndimp-P3.2**
Step	Hyp	Ref	Expression
1		ndimp-P3.2.1	. . 3 ⊢ (𝛾 → 𝜑)
2	1	axL1.AC.SH 45	. 2 ⊢ (𝛾 → (𝜓 → 𝜑))
3	2	import-P2.10a.SH 141	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