Theorem ralrimdv 3191

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  ∀wral 3141

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 209  df-an 399  df-ral 3146

This theorem is referenced by:  ralrimdva  3192  ralrimivv  3193  wefrc  5552  oneqmin  7523  nneneq  8703  cflm  9675  coflim  9686  isf32lem12  9789  axdc3lem2  9876  zorn2lem7  9927  axpre-sup  10594  zmax  12348  zbtwnre  12349  supxrunb2  12716  fzrevral  12995  lcmfdvdsb  15990  islss4  19737  topbas  21583  elcls3  21694  neips  21724  clslp  21759  subbascn  21865  cnpnei  21875  comppfsc  22143  fgss2  22485  fbflim2  22588  alexsubALTlem3  22660  alexsubALTlem4  22661  alexsubALT  22662  metcnp3  23153  aalioulem3  24926  brbtwn2  26694  hial0  28882  hial02  28883  ococss  29073  lnopmi  29780  adjlnop  29866  pjss2coi  29944  pj3cor1i  29989  strlem3a  30032  hstrlem3a  30040  mdbr3  30077  mdbr4  30078  dmdmd  30080  dmdbr3  30085  dmdbr4  30086  dmdbr5  30088  ssmd2  30092  mdslmd1i  30109  mdsymlem7  30189  cdj1i  30213  cdj3lem2b  30217  sat1el2xp  32630  fvineqsneu  34696  lub0N  36329  glb0N  36333  hlrelat2  36543  snatpsubN  36890  pmaple  36901  pclclN  37031  pclfinN  37040  pclfinclN  37090  ltrneq2  37288  trlval2  37303  trlord  37709  trintALT  41221  lindslinindsimp2  44525