Theorem ralimdva 2544

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∀wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralimdv  2545  ralimdvva  2546  f1mpt  5772  isores3  5816  caofrss  6107  caoftrn  6108  tfrlemibxssdm  6328  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  tfrcl  6365  exmidomniim  7139  exmidontri2or  7242  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  indstr  9593  caucvgre  10990  rexuz3  10999  resqrexlemgt0  11029  resqrexlemglsq  11031  cau3lem  11123  rexanre  11229  rexico  11230  2clim  11309  climcn1  11316  climcn2  11317  subcn2  11319  climsqz  11343  climsqz2  11344  climcvg1nlem  11357  fprodsplitdc  11604  bezoutlemaz  12004  bezoutlembz  12005  bezoutlembi  12006  pcfac  12348  pockthg  12355  infpnlem1  12357  isgrpinv  12926  dfgrp3me  12970  issubg4m  13053  cncnp  13733  txlm  13782  metequiv2  13999  metcnpi3  14020  rescncf  14071  cncfco  14081  suplociccreex  14105  limcresi  14138  cnplimcim  14139  cnplimclemr  14141  cnlimcim  14143  limccnpcntop  14147  limccoap  14150  2sqlem6  14470  bj-charfunbi  14566  nninffeq  14772  tridceq  14807