Theorem ralrimdv 3152

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

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

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 3062

This theorem is referenced by:  ralrimdva  3154  ralrimivv  3200  wefrc  5679  oneqmin  7820  nneneq  9246  nneneqOLD  9258  cflm  10290  coflim  10301  isf32lem12  10404  axdc3lem2  10491  zorn2lem7  10542  axpre-sup  11209  zmax  12987  zbtwnre  12988  supxrunb2  13362  fzrevral  13652  lcmfdvdsb  16680  islss4  20960  topbas  22979  elcls3  23091  neips  23121  clslp  23156  subbascn  23262  cnpnei  23272  comppfsc  23540  fgss2  23882  fbflim2  23985  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  metcnp3  24553  mpomulcn  24891  aalioulem3  26376  brbtwn2  28920  hial0  31121  hial02  31122  ococss  31312  lnopmi  32019  adjlnop  32105  pjss2coi  32183  pj3cor1i  32228  strlem3a  32271  hstrlem3a  32279  mdbr3  32316  mdbr4  32317  dmdmd  32319  dmdbr3  32324  dmdbr4  32325  dmdbr5  32327  ssmd2  32331  mdslmd1i  32348  mdsymlem7  32428  cdj1i  32452  cdj3lem2b  32456  sat1el2xp  35384  fvineqsneu  37412  lub0N  39190  glb0N  39194  hlrelat2  39405  snatpsubN  39752  pmaple  39763  pclclN  39893  pclfinN  39902  pclfinclN  39952  ltrneq2  40150  trlval2  40165  trlord  40571  trintALT  44901  lindslinindsimp2  48380