Metamath Proof Explorer

Theorem nic-idlem1

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

		Ref	Expression
	Assertion	nic-idlem1	\|- ( ( th -/\ ( ta -/\ ( ta -/\ ta ) ) ) -/\ ( ( ( ph -/\ ( ch -/\ ps ) ) -/\ th ) -/\ ( ( ph -/\ ( ch -/\ ps ) ) -/\ th ) ) )

Step	Hyp	Ref	Expression
1		nic-ax	\|- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( ph -/\ ch ) -/\ ( ( ph -/\ ph ) -/\ ( ph -/\ ph ) ) ) ) )
2	1	nic-imp	\|- ( ( th -/\ ( ta -/\ ( ta -/\ ta ) ) ) -/\ ( ( ( ph -/\ ( ch -/\ ps ) ) -/\ th ) -/\ ( ( ph -/\ ( ch -/\ ps ) ) -/\ th ) ) )

Step

Hyp

Ref

Expression

 |-  ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( ph -/\ ch ) -/\ ( ( ph -/\ ph ) -/\ ( ph -/\ ph ) ) ) ) )

 |-  ( ( th -/\ ( ta -/\ ( ta -/\ ta ) ) ) -/\ ( ( ( ph -/\ ( ch -/\ ps ) ) -/\ th ) -/\ ( ( ph -/\ ( ch -/\ ps ) ) -/\ th ) ) )