Theorem ralimdva 2564

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralimdv  2565  ralimdvva  2566  f1mpt  5821  isores3  5865  caofrss  6171  caoftrn  6172  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  tfrcl  6431  infidc  7009  exmidomniim  7216  exmidontri2or  7328  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  indstr  9686  caucvgre  11165  rexuz3  11174  resqrexlemgt0  11204  resqrexlemglsq  11206  cau3lem  11298  rexanre  11404  rexico  11405  2clim  11485  climcn1  11492  climcn2  11493  subcn2  11495  climsqz  11519  climsqz2  11520  climcvg1nlem  11533  fprodsplitdc  11780  bezoutlemaz  12197  bezoutlembz  12198  bezoutlembi  12199  pcfac  12546  pockthg  12553  infpnlem1  12555  isgrpinv  13258  dfgrp3me  13304  issubg4m  13401  mplsubgfileminv  14334  cncnp  14574  txlm  14623  metequiv2  14840  metcnpi3  14861  rescncf  14925  cncfco  14935  suplociccreex  14968  limcresi  15010  cnplimcim  15011  cnplimclemr  15013  cnlimcim  15015  limccnpcntop  15019  limccoap  15022  2sqlem6  15469  bj-charfunbi  15565  nninffeq  15775  tridceq  15813