This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem df3nandALT1

Description: The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011)

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

Proof

Step Hyp Ref Expression
1 iman 
 |-  ( ( ph -> ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) <-> -. ( ph /\ -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
2 imnan 
 |-  ( ( ps -> -. ch ) <-> -. ( ps /\ ch ) )
3 2 biimpi 
 |-  ( ( ps -> -. ch ) -> -. ( ps /\ ch ) )
4 3 3 jca 
 |-  ( ( ps -> -. ch ) -> ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) )
5 2 biimpri 
 |-  ( -. ( ps /\ ch ) -> ( ps -> -. ch ) )
6 5 adantl 
 |-  ( ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) -> ( ps -> -. ch ) )
7 4 6 impbii 
 |-  ( ( ps -> -. ch ) <-> ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) )
8 df-nan 
 |-  ( ( ps -/\ ch ) <-> -. ( ps /\ ch ) )
9 8 8 anbi12i 
 |-  ( ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) <-> ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) )
10 7 9 bitr4i 
 |-  ( ( ps -> -. ch ) <-> ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) )
11 10 imbi2i 
 |-  ( ( ph -> ( ps -> -. ch ) ) <-> ( ph -> ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
12 df-nan 
 |-  ( ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) <-> -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) )
13 12 anbi2i 
 |-  ( ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) <-> ( ph /\ -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
14 13 notbii 
 |-  ( -. ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) <-> -. ( ph /\ -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
15 1 11 14 3bitr4i 
 |-  ( ( ph -> ( ps -> -. ch ) ) <-> -. ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) )
16 df-3nand 
 |-  ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) )
17 df-nan 
 |-  ( ( ph -/\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) <-> -. ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) )
18 15 16 17 3bitr4i 
 |-  ( ( ph -/\ ps -/\ ch ) <-> ( ph -/\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) )