Theorem ralimdva 2557

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2160  ∀wral 2468

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  ralimdv  2558  ralimdvva  2559  f1mpt  5793  isores3  5837  caofrss  6132  caoftrn  6133  tfrlemibxssdm  6353  tfr1onlembxssdm  6369  tfrcllembxssdm  6382  tfrcl  6390  infidc  6965  exmidomniim  7170  exmidontri2or  7273  caucvgsrlemoffcau  7828  caucvgsrlemoffres  7830  indstr  9625  caucvgre  11025  rexuz3  11034  resqrexlemgt0  11064  resqrexlemglsq  11066  cau3lem  11158  rexanre  11264  rexico  11265  2clim  11344  climcn1  11351  climcn2  11352  subcn2  11354  climsqz  11378  climsqz2  11379  climcvg1nlem  11392  fprodsplitdc  11639  bezoutlemaz  12039  bezoutlembz  12040  bezoutlembi  12041  pcfac  12385  pockthg  12392  infpnlem1  12394  isgrpinv  13013  dfgrp3me  13059  issubg4m  13149  cncnp  14207  txlm  14256  metequiv2  14473  metcnpi3  14494  rescncf  14545  cncfco  14555  suplociccreex  14579  limcresi  14612  cnplimcim  14613  cnplimclemr  14615  cnlimcim  14617  limccnpcntop  14621  limccoap  14624  2sqlem6  14945  bj-charfunbi  15041  nninffeq  15248  tridceq  15283