Metamath Proof Explorer

Theorem norasslem3

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

Ref Expression
Assertion norasslem3 
|- ( -. ph -> ( ( ps -> ch ) <-> ( ( ph \/ ps ) -> ch ) ) )

Proof

Step Hyp Ref Expression
1 biorf 
 |-  ( -. ph -> ( ps <-> ( ph \/ ps ) ) )
2 1 imbi1d 
 |-  ( -. ph -> ( ( ps -> ch ) <-> ( ( ph \/ ps ) -> ch ) ) )