Theorem chvarfv 2241

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2394 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)

Hypotheses

Ref	Expression
chvarfv.nf	⊢ Ⅎ𝑥𝜓
chvarfv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
chvarfv.2	⊢ 𝜑

Assertion

Ref	Expression
chvarfv	⊢ 𝜓

Distinct variable group:   𝑥,𝑦

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

Proof of Theorem chvarfv

Step	Hyp	Ref	Expression
1		chvarfv.nf	. . 3 ⊢ Ⅎ𝑥𝜓
2		chvarfv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	biimpd 229	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2240	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1797	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  csbhypf  3893  axrep2  5240  axrep3  5241  isso2i  5586  frpoinsg  6319  tfindes  7842  findes  7879  dfoprab4f  8038  dom2lem  8966  frinsg  9711  pwfseqlem4a  10621  pwfseqlem4  10622  uzind4s  12874  seqof2  14032  fsumclf  15711  fsumsplitf  15715  fproddivf  15960  fprodsplitf  15961  gsumcom2  19912  mdetralt2  22503  mdetunilem2  22507  ptcldmpt  23508  elmptrab  23721  isfildlem  23751  dvmptfsum  25886  dvfsumlem2  25940  dvfsumlem2OLD  25941  lgamgulmlem2  26947  fmptcof2  32588  aciunf1lem  32593  fsumiunle  32761  esum2dlem  34089  fiunelros  34171  measiun  34215  bnj849  34922  bnj1014  34958  bnj1384  35029  bnj1489  35053  bnj1497  35057  setinds  35773  finxpreclem6  37391  ptrest  37620  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  fdc1  37747  fsumshftd  38952  fphpd  42811  monotuz  42937  monotoddzz  42939  oddcomabszz  42940  setindtrs  43021  flcidc  43166  binomcxplemnotnn0  44352  fiiuncl  45066  disjf1  45184  disjinfi  45193  supxrleubrnmptf  45454  monoordxr  45485  monoord2xr  45487  fsummulc1f  45576  fsumnncl  45577  fsumf1of  45579  fsumiunss  45580  fsumreclf  45581  fsumlessf  45582  fsumsermpt  45584  fmul01  45585  fmuldfeq  45588  fmul01lt1lem1  45589  fmul01lt1lem2  45590  fprodexp  45599  fprodabs2  45600  climmulf  45609  climexp  45610  climsuse  45613  climrecf  45614  climinff  45616  climaddf  45620  mullimc  45621  neglimc  45652  addlimc  45653  0ellimcdiv  45654  climsubmpt  45665  climreclf  45669  climeldmeqmpt  45673  climfveqmpt  45676  fnlimfvre  45679  climfveqf  45685  climfveqmpt3  45687  climeldmeqf  45688  climeqf  45693  climeldmeqmpt3  45694  climinf2  45712  climinf2mpt  45719  climinfmpt  45720  limsupequz  45728  limsupequzmptf  45736  fprodcncf  45905  dvmptmulf  45942  dvnmptdivc  45943  dvnmul  45948  dvmptfprod  45950  stoweidlem3  46008  stoweidlem34  46039  stoweidlem42  46047  stoweidlem48  46053  fourierdlem112  46223  sge0lempt  46415  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0ltfirpmpt2  46431  sge0isummpt2  46437  sge0xaddlem2  46439  sge0xadd  46440  meadjiun  46471  voliunsge0lem  46477  meaiunincf  46488  meaiuninc3  46490  meaiininc  46492  hoimbl2  46670  vonhoire  46677  vonn0ioo2  46695  vonn0icc2  46697  salpreimagtlt  46735