Metamath Proof Explorer

Theorem nic-idlem2

Description: Lemma for nic-id . Inference used by nic-id . (Contributed by Jeff Hoffman, 17-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis nic-idlem2.1 
|- ( et -/\ ( ( ph -/\ ( ch -/\ ps ) ) -/\ th ) )
Assertion nic-idlem2 
|- ( ( th -/\ ( ta -/\ ( ta -/\ ta ) ) ) -/\ et )

Proof

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