Theorem norasslem3

Description: This lemma specializes biorf suitably for the proof of norass . (Contributed by Wolf Lammen, 18-Dec-2023)

	Ref	Expression
Assertion	norasslem3	⊢ ( ¬ 𝜑 → ( ( 𝜓 → 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) → 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		biorf	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) )
2	1	imbi1d	⊢ ( ¬ 𝜑 → ( ( 𝜓 → 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) → 𝜒 ) ) )