Metamath Proof Explorer

Theorem naim2

Description: Constructor theorem for -/\ . (Contributed by Anthony Hart, 1-Sep-2011)

Ref Expression
Assertion naim2 
|- ( ( ph -> ps ) -> ( ( ch -/\ ps ) -> ( ch -/\ ph ) ) )

Proof

Step Hyp Ref Expression
1 con3 
 |-  ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
2 1 orim2d 
 |-  ( ( ph -> ps ) -> ( ( -. ch \/ -. ps ) -> ( -. ch \/ -. ph ) ) )
3 pm3.13 
 |-  ( -. ( ch /\ ps ) -> ( -. ch \/ -. ps ) )
4 pm3.14 
 |-  ( ( -. ch \/ -. ph ) -> -. ( ch /\ ph ) )
5 3 4 imim12i 
 |-  ( ( ( -. ch \/ -. ps ) -> ( -. ch \/ -. ph ) ) -> ( -. ( ch /\ ps ) -> -. ( ch /\ ph ) ) )
6 df-nan 
 |-  ( ( ch -/\ ps ) <-> -. ( ch /\ ps ) )
7 df-nan 
 |-  ( ( ch -/\ ph ) <-> -. ( ch /\ ph ) )
8 5 6 7 3imtr4g 
 |-  ( ( ( -. ch \/ -. ps ) -> ( -. ch \/ -. ph ) ) -> ( ( ch -/\ ps ) -> ( ch -/\ ph ) ) )
9 2 8 syl 
 |-  ( ( ph -> ps ) -> ( ( ch -/\ ps ) -> ( ch -/\ ph ) ) )