Metamath Proof Explorer

Theorem imnand2

Description: An -> nand relation. (Contributed by Anthony Hart, 2-Sep-2011)

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

Proof

Step Hyp Ref Expression
1 nannot 
 |-  ( -. ph <-> ( ph -/\ ph ) )
2 nannot 
 |-  ( -. ps <-> ( ps -/\ ps ) )
3 1 2 anbi12i 
 |-  ( ( -. ph /\ -. ps ) <-> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) )
4 3 notbii 
 |-  ( -. ( -. ph /\ -. ps ) <-> -. ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) )
5 iman 
 |-  ( ( -. ph -> ps ) <-> -. ( -. ph /\ -. ps ) )
6 df-nan 
 |-  ( ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) <-> -. ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) )
7 4 5 6 3bitr4i 
 |-  ( ( -. ph -> ps ) <-> ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) )