Theorem ralrimdv 3150

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 3143	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒)
4	3	ex 412	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  ralrimdva  3152  ralrimivv  3198  wefrc  5683  oneqmin  7820  nneneq  9244  nneneqOLD  9256  cflm  10288  coflim  10299  isf32lem12  10402  axdc3lem2  10489  zorn2lem7  10540  axpre-sup  11207  zmax  12985  zbtwnre  12986  supxrunb2  13359  fzrevral  13649  lcmfdvdsb  16677  islss4  20978  topbas  22995  elcls3  23107  neips  23137  clslp  23172  subbascn  23278  cnpnei  23288  comppfsc  23556  fgss2  23898  fbflim2  24001  alexsubALTlem3  24073  alexsubALTlem4  24074  alexsubALT  24075  metcnp3  24569  mpomulcn  24905  aalioulem3  26391  brbtwn2  28935  hial0  31131  hial02  31132  ococss  31322  lnopmi  32029  adjlnop  32115  pjss2coi  32193  pj3cor1i  32238  strlem3a  32281  hstrlem3a  32289  mdbr3  32326  mdbr4  32327  dmdmd  32329  dmdbr3  32334  dmdbr4  32335  dmdbr5  32337  ssmd2  32341  mdslmd1i  32358  mdsymlem7  32438  cdj1i  32462  cdj3lem2b  32466  sat1el2xp  35364  fvineqsneu  37394  lub0N  39171  glb0N  39175  hlrelat2  39386  snatpsubN  39733  pmaple  39744  pclclN  39874  pclfinN  39883  pclfinclN  39933  ltrneq2  40131  trlval2  40146  trlord  40552  trintALT  44879  lindslinindsimp2  48309