Theorem ralrimdv 3138

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralrimdva  3140  ralrimivv  3185  wefrc  5648  oneqmin  7794  nneneq  9220  cflm  10264  coflim  10275  isf32lem12  10378  axdc3lem2  10465  zorn2lem7  10516  axpre-sup  11183  zmax  12961  zbtwnre  12962  supxrunb2  13336  fzrevral  13629  lcmfdvdsb  16662  islss4  20919  topbas  22910  elcls3  23021  neips  23051  clslp  23086  subbascn  23192  cnpnei  23202  comppfsc  23470  fgss2  23812  fbflim2  23915  alexsubALTlem3  23987  alexsubALTlem4  23988  alexsubALT  23989  metcnp3  24479  mpomulcn  24809  aalioulem3  26294  onsfi  28299  brbtwn2  28884  hial0  31083  hial02  31084  ococss  31274  lnopmi  31981  adjlnop  32067  pjss2coi  32145  pj3cor1i  32190  strlem3a  32233  hstrlem3a  32241  mdbr3  32278  mdbr4  32279  dmdmd  32281  dmdbr3  32286  dmdbr4  32287  dmdbr5  32289  ssmd2  32293  mdslmd1i  32310  mdsymlem7  32390  cdj1i  32414  cdj3lem2b  32418  sat1el2xp  35401  fvineqsneu  37429  lub0N  39207  glb0N  39211  hlrelat2  39422  snatpsubN  39769  pmaple  39780  pclclN  39910  pclfinN  39919  pclfinclN  39969  ltrneq2  40167  trlval2  40182  trlord  40588  trintALT  44905  lindslinindsimp2  48439