Theorem ralimdva 2573

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 1551	. 2 ⊢ Ⅎ𝑥𝜑
2		ralimdva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	1, 2	ralimdaa 2572	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2176  ∀wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralimdv  2574  ralimdvva  2575  f1mpt  5840  isores3  5884  caofrss  6190  caoftrn  6191  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  tfrcl  6450  infidc  7036  exmidomniim  7243  exmidontri2or  7355  caucvgsrlemoffcau  7911  caucvgsrlemoffres  7913  indstr  9714  caucvgre  11292  rexuz3  11301  resqrexlemgt0  11331  resqrexlemglsq  11333  cau3lem  11425  rexanre  11531  rexico  11532  2clim  11612  climcn1  11619  climcn2  11620  subcn2  11622  climsqz  11646  climsqz2  11647  climcvg1nlem  11660  fprodsplitdc  11907  bezoutlemaz  12324  bezoutlembz  12325  bezoutlembi  12326  pcfac  12673  pockthg  12680  infpnlem1  12682  isgrpinv  13386  dfgrp3me  13432  issubg4m  13529  mplsubgfileminv  14462  cncnp  14702  txlm  14751  metequiv2  14968  metcnpi3  14989  rescncf  15053  cncfco  15063  suplociccreex  15096  limcresi  15138  cnplimcim  15139  cnplimclemr  15141  cnlimcim  15143  limccnpcntop  15147  limccoap  15150  2sqlem6  15597  bj-charfunbi  15747  nninffeq  15957  tridceq  15995