Theorem chvar 1530

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

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298

This theorem is referenced by:  axrep2 3430  axrep3 3431  tfis 3938  tfindes 3946  findes 3983  cnvopabOLD 4318  tz6.12f 4695  dom2d 5463  ordtypelem7 5690  zfcndrep 6118  uzind4s 7621  uzind4s2 7622  iscaunns 9222  bnj1306 13049  bnj1310 13050  bnj1492 13161  bnj1014 13374  bnj1332 13499  bnj1375 13509  bnj1376 13510  setinds 13844  wfisg 13917  frinsg 13941  hbprod 14660  fgsb 14921  ordtypelem7OLD 15381  fdc1 15813  oprpiece1res2 15881  cncfres 15895  cnresoprab 15915

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-9o 1481

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain