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	|- ( ( ( ph \/ ps ) -> ch ) <-> ( ( ph -\/ ps ) \/ ch ) )

Proof

Step	Hyp	Ref	Expression
1		imor	|- ( ( ( ph \/ ps ) -> ch ) <-> ( -. ( ph \/ ps ) \/ ch ) )
2		df-nor	|- ( ( ph -\/ ps ) <-> -. ( ph \/ ps ) )
3	2	orbi1i	|- ( ( ( ph -\/ ps ) \/ ch ) <-> ( -. ( ph \/ ps ) \/ ch ) )
4	1 3	bitr4i	|- ( ( ( ph \/ ps ) -> ch ) <-> ( ( ph -\/ ps ) \/ ch ) )