Theorem ralimdva 2575

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2178  ∀wral 2486

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  ralimdv  2576  ralimdvva  2577  f1mpt  5863  isores3  5907  caofrss  6213  caoftrn  6214  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  tfrcl  6473  infidc  7062  exmidomniim  7269  exmidontri2or  7389  caucvgsrlemoffcau  7946  caucvgsrlemoffres  7948  indstr  9749  caucvgre  11407  rexuz3  11416  resqrexlemgt0  11446  resqrexlemglsq  11448  cau3lem  11540  rexanre  11646  rexico  11647  2clim  11727  climcn1  11734  climcn2  11735  subcn2  11737  climsqz  11761  climsqz2  11762  climcvg1nlem  11775  fprodsplitdc  12022  bezoutlemaz  12439  bezoutlembz  12440  bezoutlembi  12441  pcfac  12788  pockthg  12795  infpnlem1  12797  isgrpinv  13501  dfgrp3me  13547  issubg4m  13644  mplsubgfileminv  14577  cncnp  14817  txlm  14866  metequiv2  15083  metcnpi3  15104  rescncf  15168  cncfco  15178  suplociccreex  15211  limcresi  15253  cnplimcim  15254  cnplimclemr  15256  cnlimcim  15258  limccnpcntop  15262  limccoap  15265  2sqlem6  15712  bj-charfunbi  15946  nninffeq  16159  tridceq  16197