Theorem bijust-P2.2 106

Description: Justification Theorem for df-bi-D2.1 107.

Assertion

Ref	Expression
bijust-P2.2	⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))

Proof of Theorem bijust-P2.2

Step	Hyp	Ref	Expression
1		bijust-P2.2-L1 105	1 ⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))

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)