Theorem ralimdva 2544

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∀wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralimdv  2545  ralimdvva  2546  f1mpt  5771  isores3  5815  caofrss  6106  caoftrn  6107  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  tfrcl  6364  exmidomniim  7138  exmidontri2or  7241  caucvgsrlemoffcau  7796  caucvgsrlemoffres  7798  indstr  9592  caucvgre  10989  rexuz3  10998  resqrexlemgt0  11028  resqrexlemglsq  11030  cau3lem  11122  rexanre  11228  rexico  11229  2clim  11308  climcn1  11315  climcn2  11316  subcn2  11318  climsqz  11342  climsqz2  11343  climcvg1nlem  11356  fprodsplitdc  11603  bezoutlemaz  12003  bezoutlembz  12004  bezoutlembi  12005  pcfac  12347  pockthg  12354  infpnlem1  12356  isgrpinv  12925  dfgrp3me  12969  issubg4m  13051  cncnp  13700  txlm  13749  metequiv2  13966  metcnpi3  13987  rescncf  14038  cncfco  14048  suplociccreex  14072  limcresi  14105  cnplimcim  14106  cnplimclemr  14108  cnlimcim  14110  limccnpcntop  14114  limccoap  14117  2sqlem6  14437  bj-charfunbi  14533  nninffeq  14739  tridceq  14774