Metamath Proof Explorer

Theorem nic-luk2

Description: Proof of luk-2 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-luk2 
|- ( ( -. ph -> ph ) -> ph )

Proof

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