Theorem chvarv 2361

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)

Hypotheses

Ref	Expression
chvarv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
chvarv.2	⊢ 𝜑

Assertion

Ref	Expression
chvarv	⊢ 𝜓

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem chvarv

Step	Hyp	Ref	Expression
1		nfv 1957	. 2 ⊢ Ⅎ𝑥𝜓
2		chvarv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		chvarv.2	. 2 ⊢ 𝜑
4	1, 2, 3	chvar 2360	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-12 2163  ax-13 2334

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-nf 1828

This theorem is referenced by:  axext3ALT  2757  axrep1  5009  axsep2  5020  isso2i  5310  tz6.12f  6472  dfac12lem2  9303  wunex2  9897  ltordlem  10903  prodfdiv  15040  iscatd2  16738  yoniso  17322  mrcmndind  17763  gsum2dlem2  18767  isdrngrd  19176  frlmphl  20535  frlmup1  20552  mdetralt  20830  mdetunilem9  20842  neiptoptop  21354  neiptopnei  21355  cnextcn  22290  cnextfres1  22291  ustuqtop4  22467  dscmet  22796  nrmmetd  22798  rolle  24201  numclwlk2lem2f1o  27824  numclwlk2lem2f1oOLD  27827  chscllem2  29086  esumcvg  30754  eulerpartlemgvv  31044  eulerpartlemn  31049  bnj1326  31701  fwddifnp1  32869  poimirlem13  34057  poimirlem14  34058  poimirlem25  34069  poimirlem31  34075  ftc1anclem7  34125  ftc1anc  34127  fdc  34174  fdc1  34175  iscringd  34430  ismrcd2  38236  fphpdo  38355  monotoddzzfi  38480  monotoddzz  38481  mendlmod  38736  dvgrat  39481  cvgdvgrat  39482  binomcxplemnotnn0  39525  iunincfi  40217  wessf1ornlem  40308  monoords  40434  limcperiod  40782  sumnnodd  40784  cncfshift  41029  cncfperiod  41034  icccncfext  41042  fperdvper  41075  dvnprodlem1  41103  dvnprodlem2  41104  dvnprodlem3  41105  iblspltprt  41130  itgspltprt  41136  stoweidlem43  41201  stoweidlem62  41220  dirkercncflem2  41262  fourierdlem12  41277  fourierdlem15  41280  fourierdlem34  41299  fourierdlem41  41306  fourierdlem42  41307  fourierdlem48  41312  fourierdlem50  41314  fourierdlem51  41315  fourierdlem73  41337  fourierdlem79  41343  fourierdlem81  41345  fourierdlem83  41347  fourierdlem92  41356  fourierdlem94  41358  fourierdlem103  41367  fourierdlem104  41368  fourierdlem111  41375  fourierdlem112  41376  fourierdlem113  41377  etransclem2  41394  etransclem46  41438  intsaluni  41485  meaiuninclem  41635  meaiuninc3v  41639  meaiininclem  41641  ovn0lem  41720  hoidmvlelem2  41751  hoidmvlelem3  41752  hspmbllem2  41782  vonioo  41837  vonicc  41840  pimincfltioc  41867  smflimlem4  41923