Theorem iidn3 1270

Description: idn3 16510 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.)

Assertion

Ref	Expression
iidn3	|- (ph -> (ps -> (ch -> ch)))

Proof of Theorem iidn3

Step	Hyp	Ref	Expression
1		id 73	. 2 |- (ch -> ch)
2	1	a1i12 9	1 |- (ph -> (ps -> (ch -> ch)))

Syntax hints:   -> wi 3

This theorem is referenced by:  en3lplem2 5757  trintALT 16705

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain