ndasm-P3.1 - bfol.mm Proof Explorer

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

Theorem ndasm-P3.1 166

Description: Natural Deduction: State Assumption.

This rule is simply stating an assumption.

**Assertion**
Ref	Expression
ndasm-P3.1	⊢ ((𝛾 ∧ 𝜑) → 𝜑)

**Proof of Theorem ndasm-P3.1**
Step	Hyp	Ref	Expression
1		simpr-P2.9b 136	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

This theorem is referenced by: ndfalsei-P3.19 184 rcp-NDASM1of1 192 rcp-NDASM2of2 194 rcp-NDASM3of3 197 rcp-NDASM4of4 201 rcp-NDASM5of5 206