Theorem cmb-L2.3 99

Description: Combining Lemma.

Assertion

Ref	Expression
cmb-L2.3	⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))

Proof of Theorem cmb-L2.3

Step	Hyp	Ref	Expression
1		id-P1.4 36	. 2 ⊢ (¬ (𝜑 → ¬ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
2	1	export-L2.1b.SH 94	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:  cmb-L2.3.2SH  100  bicmb-P2.5c  119  cmb-P2.9c  138