Theorem ralrimdv 3135

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.)

Hypothesis

Ref	Expression
ralrimdv.1	⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜓,𝑥

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

Proof of Theorem ralrimdv

Step	Hyp	Ref	Expression
1		ralrimdv.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))
2	1	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒))
3	2	ralrimiv 3128	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒)
4	3	ex 412	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  ralrimdva  3137  ralrimivv  3178  wefrc  5619  oneqmin  7747  nneneq  9134  cflm  10164  coflim  10175  isf32lem12  10278  axdc3lem2  10365  zorn2lem7  10416  axpre-sup  11084  zmax  12862  zbtwnre  12863  supxrunb2  13239  fzrevral  13532  lcmfdvdsb  16574  islss4  20917  topbas  22920  elcls3  23031  neips  23061  clslp  23096  subbascn  23202  cnpnei  23212  comppfsc  23480  fgss2  23822  fbflim2  23925  alexsubALTlem3  23997  alexsubALTlem4  23998  alexsubALT  23999  metcnp3  24488  mpomulcn  24818  aalioulem3  26302  onsfi  28356  brbtwn2  28982  hial0  31181  hial02  31182  ococss  31372  lnopmi  32079  adjlnop  32165  pjss2coi  32243  pj3cor1i  32288  strlem3a  32331  hstrlem3a  32339  mdbr3  32376  mdbr4  32377  dmdmd  32379  dmdbr3  32384  dmdbr4  32385  dmdbr5  32387  ssmd2  32391  mdslmd1i  32408  mdsymlem7  32488  cdj1i  32512  cdj3lem2b  32516  rankfilimb  35260  sat1el2xp  35575  fvineqsneu  37618  lub0N  39517  glb0N  39521  hlrelat2  39731  snatpsubN  40078  pclclN  40219  pclfinN  40228  pclfinclN  40278  ltrneq2  40476  trlval2  40491  trlord  40897  trintALT  45188  lindslinindsimp2  48776