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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2050  ∀wral 3088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ral 3093

This theorem is referenced by:  ralrimdva  3139  ralrimivv  3140  wefrc  5402  oneqmin  7338  nneneq  8498  cflm  9472  coflim  9483  isf32lem12  9586  axdc3lem2  9673  zorn2lem7  9724  axpre-sup  10391  zmax  12162  zbtwnre  12163  supxrunb2  12532  fzrevral  12811  lcmfdvdsb  15846  islss4  19459  topbas  21287  elcls3  21398  neips  21428  clslp  21463  subbascn  21569  cnpnei  21579  comppfsc  21847  fgss2  22189  fbflim2  22292  alexsubALTlem3  22364  alexsubALTlem4  22365  alexsubALT  22366  metcnp3  22856  aalioulem3  24629  brbtwn2  26397  hial0  28661  hial02  28662  ococss  28854  lnopmi  29561  adjlnop  29647  pjss2coi  29725  pj3cor1i  29770  strlem3a  29813  hstrlem3a  29821  mdbr3  29858  mdbr4  29859  dmdmd  29861  dmdbr3  29866  dmdbr4  29867  dmdbr5  29869  ssmd2  29873  mdslmd1i  29890  mdsymlem7  29970  cdj1i  29994  cdj3lem2b  29998  sat1el2xp  32189  fvineqsneu  34133  lub0N  35770  glb0N  35774  hlrelat2  35984  snatpsubN  36331  pmaple  36342  pclclN  36472  pclfinN  36481  pclfinclN  36531  ltrneq2  36729  trlval2  36744  trlord  37150  trintALT  40634  lindslinindsimp2  43886