Metamath Proof Explorer

Theorem nic-luk3

Description: Proof of luk-3 from nic-ax and nic-mp . (Contributed by Jeff Hoffman, 18-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nic-luk3 
|- ( ph -> ( -. ph -> ps ) )

Proof

Step Hyp Ref Expression
1 nic-dfim 
 |-  ( ( ( -. ph -/\ ( ps -/\ ps ) ) -/\ ( -. ph -> ps ) ) -/\ ( ( ( -. ph -/\ ( ps -/\ ps ) ) -/\ ( -. ph -/\ ( ps -/\ ps ) ) ) -/\ ( ( -. ph -> ps ) -/\ ( -. ph -> ps ) ) ) )
2 1 nic-bi1 
 |-  ( ( -. ph -/\ ( ps -/\ ps ) ) -/\ ( ( -. ph -> ps ) -/\ ( -. ph -> ps ) ) )
3 nic-dfneg 
 |-  ( ( ( ph -/\ ph ) -/\ -. ph ) -/\ ( ( ( ph -/\ ph ) -/\ ( ph -/\ ph ) ) -/\ ( -. ph -/\ -. ph ) ) )
4 3 nic-bi2 
 |-  ( -. ph -/\ ( ( ph -/\ ph ) -/\ ( ph -/\ ph ) ) )
5 nic-id 
 |-  ( ph -/\ ( ph -/\ ph ) )
6 4 5 nic-iimp1 
 |-  ( ph -/\ -. ph )
7 2 6 nic-iimp2 
 |-  ( ph -/\ ( ( -. ph -> ps ) -/\ ( -. ph -> ps ) ) )
8 nic-dfim 
 |-  ( ( ( ph -/\ ( ( -. ph -> ps ) -/\ ( -. ph -> ps ) ) ) -/\ ( ph -> ( -. ph -> ps ) ) ) -/\ ( ( ( ph -/\ ( ( -. ph -> ps ) -/\ ( -. ph -> ps ) ) ) -/\ ( ph -/\ ( ( -. ph -> ps ) -/\ ( -. ph -> ps ) ) ) ) -/\ ( ( ph -> ( -. ph -> ps ) ) -/\ ( ph -> ( -. ph -> ps ) ) ) ) )
9 8 nic-bi1 
 |-  ( ( ph -/\ ( ( -. ph -> ps ) -/\ ( -. ph -> ps ) ) ) -/\ ( ( ph -> ( -. ph -> ps ) ) -/\ ( ph -> ( -. ph -> ps ) ) ) )
10 7 9 nic-mp 
 |-  ( ph -> ( -. ph -> ps ) )