Theorem ralrimdv 3070

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2103  ∀wral 3014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 3019

This theorem is referenced by:  ralrimdva  3071  ralrimivv  3072  wefrc  5212  oneqmin  7122  nneneq  8259  cflm  9185  coflim  9196  isf32lem12  9299  axdc3lem2  9386  zorn2lem7  9437  axpre-sup  10103  zmax  11899  zbtwnre  11900  supxrunb2  12264  fzrevral  12539  islss4  19085  topbas  20899  elcls3  21010  neips  21040  clslp  21075  subbascn  21181  cnpnei  21191  comppfsc  21458  fgss2  21800  fbflim2  21903  alexsubALTlem3  21975  alexsubALTlem4  21976  alexsubALT  21977  metcnp3  22467  aalioulem3  24209  brbtwn2  25905  hial0  28189  hial02  28190  ococss  28382  lnopmi  29089  adjlnop  29175  pjss2coi  29253  pj3cor1i  29298  strlem3a  29341  hstrlem3a  29349  mdbr3  29386  mdbr4  29387  dmdmd  29389  dmdbr3  29394  dmdbr4  29395  dmdbr5  29397  ssmd2  29401  mdslmd1i  29418  mdsymlem7  29498  cdj1i  29522  cdj3lem2b  29526  lub0N  34896  glb0N  34900  hlrelat2  35109  snatpsubN  35456  pmaple  35467  pclclN  35597  pclfinN  35606  pclfinclN  35656  ltrneq2  35854  trlval2  35870  trlord  36276  trintALT  39533  lindslinindsimp2  42679