Theorem chvar 1167

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 153	. . 3 |- (x = y -> (ph -> ps))
4	1, 3	a4im 1159	. 2 |- (A.xph -> ps)
5		chv2.3	. 2 |- ph
6	4, 5	mpg 986	1 |- ps

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956

This theorem is referenced by:  axrep2 2695  axrep3 2696  tfis 3127  findes 3160  tfindes 3164  cnvopab 3445  tz6.12f 3738  dom2d 4404  zfcndrep 4966  uzind4s 6452  uzind4s2 6453  iscaunns 7944  fgsb 10570  fgsbOLD 10571

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-9o 1123

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain