Theorem ralimdv 3177

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1831). (Contributed by NM, 8-Oct-2003.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	adantr 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 3175	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2143  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3078

This theorem is referenced by:  r19.21v  3188  ralimdvv  3212  ss2ralv  4008  poss  5558  sess1  5613  sess2  5614  riinint  5949  iinpreima  7051  dffo4  7085  dffo5  7086  isoini2  7324  tfindsg  7842  el2mpocsbcl  8065  xpord3inddlem  8135  iiner  8772  xpf1o  9112  dffi3  9378  brwdom3  9531  xpwdomg  9534  ttrclss  9676  bndrank  9800  cfub  10206  cff1  10216  cfflb  10217  cfslb2n  10226  cofsmo  10227  cfcoflem  10230  pwcfsdom  10542  fpwwe2lem12  10601  inawinalem  10648  grupr  10756  fsequb  13989  cau3lem  15383  caubnd2  15386  caubnd  15387  rlim2lt  15525  rlim3  15526  climshftlem  15602  climcau  15699  caucvgb  15708  serf0  15709  modfsummods  15822  cvgcmp  15845  mreriincl  17627  acsfn1c  17695  resspos  18462  resstos  18463  chnrss  18648  islss4  21030  riinopn  22969  fiinbas  23013  baspartn  23015  isclo2  23149  lmcls  23363  lmcnp  23365  isnrm3  23420  1stcelcls  23522  llyss  23540  nllyss  23541  ptpjpre1  23632  txlly  23697  txnlly  23698  tx1stc  23711  xkococnlem  23720  fbunfip  23930  filssufilg  23972  cnpflf2  24061  fcfnei  24096  isucn2  24339  rescncf  24960  lebnum  25027  cfilss  25333  fgcfil  25334  iscau4  25342  cmetcaulem  25351  caussi  25360  ovolunlem1  25560  ulmclm  26451  ulmcaulem  26458  ulmcau  26459  ulmss  26461  rlimcnp  27031  cxploglim  27043  2sqreunnlem2  27520  pntlemp  27675  nosupno  27768  nosupres  27772  noinfno  27783  noinfres  27787  ssslts2  27868  madebdayim  27982  madebdaylemold  27992  axcontlem4  29169  ewlkle  29807  uspgr2wlkeq  29847  umgrwlknloop  29850  wlkiswwlksupgr2  30078  3cyclfrgrrn2  30490  nmlnoubi  31000  lnon0  31002  disjpreima  32785  submarchi  33367  prmidl2  33628  crefss  34147  r1filimi  35400  iccllysconn  35601  cvmlift2lem1  35653  dmopab3rexdif  35756  ss2mcls  35919  mclsax  35920  dfttc4lem2  36890  isinf2  37900  poimirlem25  38145  poimirlem27  38147  upixp  38229  caushft  38261  sstotbnd3  38276  totbndss  38277  unichnidl  38531  ispridl2  38538  elrfirn2  43278  mzpsubst  43330  eluzrabdioph  43384  neik0pk1imk0  44624  mnuop3d  44848  ismnushort  44878  pwclaxpow  45561  limsupub  46279  limsupre3lem  46307  climuzlem  46318  xlimbr  46402  fourierdlem103  46784  fourierdlem104  46785  qndenserrnbllem  46869  2reuimp  47710  ralralimp  47873