Theorem chvar 1166

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 1158	. 2 |- (A.xph -> ps)
5		chv2.3	. 2 |- ph
6	4, 5	mpg 985	1 |- ps

Syntax hints:   -> wi 3   <-> wb 146  A.wal 953   = wceq 955

This theorem is referenced by:  axrep2 2691  axrep3 2692  tfis 3123  findes 3156  tfindes 3160  cnvopab 3441  tz6.12f 3733  dom2d 4394  zfcndrep 4949  uzind4s 6397  uzind4s2 6398  iscaunns 7906  fgsb 10503

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974  ax-9o 1122

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain