Theorem ralimdva 2542

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2146  ∀wral 2453

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458

This theorem is referenced by:  ralimdv  2543  ralimdvva  2544  f1mpt  5762  isores3  5806  caofrss  6097  caoftrn  6098  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  tfrcl  6355  exmidomniim  7129  exmidontri2or  7232  caucvgsrlemoffcau  7772  caucvgsrlemoffres  7774  indstr  9564  caucvgre  10956  rexuz3  10965  resqrexlemgt0  10995  resqrexlemglsq  10997  cau3lem  11089  rexanre  11195  rexico  11196  2clim  11275  climcn1  11282  climcn2  11283  subcn2  11285  climsqz  11309  climsqz2  11310  climcvg1nlem  11323  fprodsplitdc  11570  bezoutlemaz  11969  bezoutlembz  11970  bezoutlembi  11971  pcfac  12313  pockthg  12320  infpnlem1  12322  isgrpinv  12786  dfgrp3me  12829  cncnp  13299  txlm  13348  metequiv2  13565  metcnpi3  13586  rescncf  13637  cncfco  13647  suplociccreex  13671  limcresi  13704  cnplimcim  13705  cnplimclemr  13707  cnlimcim  13709  limccnpcntop  13713  limccoap  13716  2sqlem6  14025  bj-charfunbi  14121  nninffeq  14328  tridceq  14363