Theorem ralimdva 2609

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdva

Step	Hyp	Ref	Expression
1		nfv 1577	. 2 ⊢ Ⅎ𝑥𝜑
2		ralimdva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	1, 2	ralimdaa 2608	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ∀wral 2520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525

This theorem is referenced by:  ralimdv  2610  ralimdvva  2611  f1mpt  5944  isores3  5988  caofrss  6298  caoftrn  6299  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  tfrcl  6595  infidc  7201  exmidomniim  7432  exmidontri2or  7553  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  indstr  9925  caucvgre  11666  rexuz3  11675  resqrexlemgt0  11705  resqrexlemglsq  11707  cau3lem  11799  rexanre  11905  rexico  11906  2clim  11986  climcn1  11993  climcn2  11994  subcn2  11996  climsqz  12020  climsqz2  12021  climcvg1nlem  12034  fprodsplitdc  12282  bezoutlemaz  12699  bezoutlembz  12700  bezoutlembi  12701  pcfac  13048  pockthg  13055  infpnlem1  13057  isgrpinv  13767  dfgrp3me  13813  issubg4m  13910  mplsubgfileminv  14855  cncnp  15095  txlm  15144  metequiv2  15361  metcnpi3  15382  rescncf  15446  cncfco  15456  suplociccreex  15489  limcresi  15531  cnplimcim  15532  cnplimclemr  15534  cnlimcim  15536  limccnpcntop  15540  limccoap  15543  2sqlem6  15993  wlkvtxiedg  16340  wlkvtxiedgg  16341  upgrwlkvtxedg  16359  uspgr2wlkeq  16360  clwwlkccatlem  16395  bj-charfunbi  16581  nninffeq  16798  tridceq  16841