Metamath Proof Explorer


Theorem naim1

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

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

Proof

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