Theorem ralrimdv 3190

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3145

This theorem is referenced by:  ralrimdva  3191  ralrimivv  3192  wefrc  5551  oneqmin  7522  nneneq  8702  cflm  9674  coflim  9685  isf32lem12  9788  axdc3lem2  9875  zorn2lem7  9926  axpre-sup  10593  zmax  12348  zbtwnre  12349  supxrunb2  12716  fzrevral  12995  lcmfdvdsb  15989  islss4  19736  topbas  21582  elcls3  21693  neips  21723  clslp  21758  subbascn  21864  cnpnei  21874  comppfsc  22142  fgss2  22484  fbflim2  22587  alexsubALTlem3  22659  alexsubALTlem4  22660  alexsubALT  22661  metcnp3  23152  aalioulem3  24925  brbtwn2  26693  hial0  28881  hial02  28882  ococss  29072  lnopmi  29779  adjlnop  29865  pjss2coi  29943  pj3cor1i  29988  strlem3a  30031  hstrlem3a  30039  mdbr3  30076  mdbr4  30077  dmdmd  30079  dmdbr3  30084  dmdbr4  30085  dmdbr5  30087  ssmd2  30091  mdslmd1i  30108  mdsymlem7  30188  cdj1i  30212  cdj3lem2b  30216  sat1el2xp  32628  fvineqsneu  34694  lub0N  36327  glb0N  36331  hlrelat2  36541  snatpsubN  36888  pmaple  36899  pclclN  37029  pclfinN  37038  pclfinclN  37088  ltrneq2  37286  trlval2  37301  trlord  37707  trintALT  41222  lindslinindsimp2  44525