Metamath Proof Explorer

Theorem nic-id

Description: Theorem id expressed with -/\ . (Contributed by Jeff Hoffman, 17-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nic-id 
|- ( ta -/\ ( ta -/\ ta ) )

Proof

Step Hyp Ref Expression
1 nic-ax 
 |-  ( ( ps -/\ ( ps -/\ ps ) ) -/\ ( ( th -/\ ( th -/\ th ) ) -/\ ( ( ph -/\ ps ) -/\ ( ( ps -/\ ph ) -/\ ( ps -/\ ph ) ) ) ) )
2 1 nic-idlem2 
 |-  ( ( ( ( ph -/\ ps ) -/\ ( ( ps -/\ ph ) -/\ ( ps -/\ ph ) ) ) -/\ ( ch -/\ ( ch -/\ ch ) ) ) -/\ ( ps -/\ ( ps -/\ ps ) ) )
3 nic-idlem1 
 |-  ( ( ( ch -/\ ( ch -/\ ch ) ) -/\ ( ta -/\ ( ta -/\ ta ) ) ) -/\ ( ( ( ( ph -/\ ps ) -/\ ( ( ps -/\ ph ) -/\ ( ps -/\ ph ) ) ) -/\ ( ch -/\ ( ch -/\ ch ) ) ) -/\ ( ( ( ph -/\ ps ) -/\ ( ( ps -/\ ph ) -/\ ( ps -/\ ph ) ) ) -/\ ( ch -/\ ( ch -/\ ch ) ) ) ) )
4 3 nic-idlem2 
 |-  ( ( ( ( ( ph -/\ ps ) -/\ ( ( ps -/\ ph ) -/\ ( ps -/\ ph ) ) ) -/\ ( ch -/\ ( ch -/\ ch ) ) ) -/\ ( ps -/\ ( ps -/\ ps ) ) ) -/\ ( ( ch -/\ ( ch -/\ ch ) ) -/\ ( ta -/\ ( ta -/\ ta ) ) ) )
5 2 4 nic-mp 
 |-  ( ta -/\ ( ta -/\ ta ) )