Metamath Proof Explorer


Theorem norasslem1

Description: This lemma shows the equivalence of two expressions, used in norass . (Contributed by Wolf Lammen, 18-Dec-2023)

Ref Expression
Assertion norasslem1 ( ( ( 𝜑𝜓 ) → 𝜒 ) ↔ ( ( 𝜑 𝜓 ) ∨ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 imor ( ( ( 𝜑𝜓 ) → 𝜒 ) ↔ ( ¬ ( 𝜑𝜓 ) ∨ 𝜒 ) )
2 df-nor ( ( 𝜑 𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
3 2 orbi1i ( ( ( 𝜑 𝜓 ) ∨ 𝜒 ) ↔ ( ¬ ( 𝜑𝜓 ) ∨ 𝜒 ) )
4 1 3 bitr4i ( ( ( 𝜑𝜓 ) → 𝜒 ) ↔ ( ( 𝜑 𝜓 ) ∨ 𝜒 ) )