mbirev-P2.1b - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > mbirev-P2.1b

Theorem mbirev-P2.1b 102

Description: Motivation for ↔ Definition, Part B.

**Hypothesis**
Ref	Expression
mbirev-P2.1b.1	⊢ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))

**Assertion**
Ref	Expression
mbirev-P2.1b	⊢ (𝜓 → 𝜑)

**Proof of Theorem mbirev-P2.1b**
Step	Hyp	Ref	Expression
1		mbirev-P2.1b.1	. 2 ⊢ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))
2	1	simpr-L2.2b.SH 98	1 ⊢ (𝜓 → 𝜑)

Colors of variables: wff objvar term class

Syntax hints: ¬ wff-neg 9 → wff-imp 10

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

This theorem is referenced by: (None)