Theorem chvar 1204

Description: Implicit substitution of y for x into a theorem. (Contributed by Raph Levien, 9-Jul-2003.)

Hypotheses

Ref	Expression
chv2.1	|- (ps -> A.xps)
chv2.2	|- (x = y -> (ph <-> ps))
chv2.3	|- ph

Assertion

Ref	Expression
chvar	|- ps

Proof of Theorem chvar

Step	Hyp	Ref	Expression
1		chv2.1	. . 3 |- (ps -> A.xps)
2		chv2.2	. . . 4 |- (x = y -> (ph <-> ps))
3	2	biimpd 151	. . 3 |- (x = y -> (ph -> ps))
4	1, 3	a4im 1196	. 2 |- (A.xph -> ps)
5		chv2.3	. 2 |- ph
6	4, 5	mpg 1022	1 |- ps

Syntax hints:   -> wi 3   <-> wb 144  A.wal 990   = wceq 992

This theorem is referenced by:  axrep2 2769  axrep3 2770  tfis 3208  tfindes 3215  findes 3248  cnvopab 3537  tz6.12f 3849  dom2d 4545  zfcndrep 5120  uzind4s 6579  uzind4s2 6580  iscaunns 8155  fgsb 11082  ordtypelem7 11433  cncfres 11956

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011  ax-9o 1159

This theorem depends on definitions:  df-bi 145

Copyright terms: Public domain