Theorem ralimdva 2561

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 2560	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  ∀wral 2472

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 2477

This theorem is referenced by:  ralimdv  2562  ralimdvva  2563  f1mpt  5814  isores3  5858  caofrss  6157  caoftrn  6158  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  tfrcl  6417  infidc  6993  exmidomniim  7200  exmidontri2or  7303  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  indstr  9658  caucvgre  11125  rexuz3  11134  resqrexlemgt0  11164  resqrexlemglsq  11166  cau3lem  11258  rexanre  11364  rexico  11365  2clim  11444  climcn1  11451  climcn2  11452  subcn2  11454  climsqz  11478  climsqz2  11479  climcvg1nlem  11492  fprodsplitdc  11739  bezoutlemaz  12140  bezoutlembz  12141  bezoutlembi  12142  pcfac  12488  pockthg  12495  infpnlem1  12497  isgrpinv  13126  dfgrp3me  13172  issubg4m  13263  cncnp  14398  txlm  14447  metequiv2  14664  metcnpi3  14685  rescncf  14736  cncfco  14746  suplociccreex  14778  limcresi  14820  cnplimcim  14821  cnplimclemr  14823  cnlimcim  14825  limccnpcntop  14829  limccoap  14832  2sqlem6  15207  bj-charfunbi  15303  nninffeq  15510  tridceq  15546