Theorem ralimdva 2572

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2175  ∀wral 2483

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488

This theorem is referenced by:  ralimdv  2573  ralimdvva  2574  f1mpt  5839  isores3  5883  caofrss  6189  caoftrn  6190  tfrlemibxssdm  6412  tfr1onlembxssdm  6428  tfrcllembxssdm  6441  tfrcl  6449  infidc  7035  exmidomniim  7242  exmidontri2or  7354  caucvgsrlemoffcau  7910  caucvgsrlemoffres  7912  indstr  9713  caucvgre  11263  rexuz3  11272  resqrexlemgt0  11302  resqrexlemglsq  11304  cau3lem  11396  rexanre  11502  rexico  11503  2clim  11583  climcn1  11590  climcn2  11591  subcn2  11593  climsqz  11617  climsqz2  11618  climcvg1nlem  11631  fprodsplitdc  11878  bezoutlemaz  12295  bezoutlembz  12296  bezoutlembi  12297  pcfac  12644  pockthg  12651  infpnlem1  12653  isgrpinv  13357  dfgrp3me  13403  issubg4m  13500  mplsubgfileminv  14433  cncnp  14673  txlm  14722  metequiv2  14939  metcnpi3  14960  rescncf  15024  cncfco  15034  suplociccreex  15067  limcresi  15109  cnplimcim  15110  cnplimclemr  15112  cnlimcim  15114  limccnpcntop  15118  limccoap  15121  2sqlem6  15568  bj-charfunbi  15709  nninffeq  15919  tridceq  15957