Theorem ralrimdv 2997

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2030  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

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

This theorem is referenced by:  ralrimdva  2998  ralrimivv  2999  wefrc  5137  oneqmin  7047  nneneq  8184  cflm  9110  coflim  9121  isf32lem12  9224  axdc3lem2  9311  zorn2lem7  9362  axpre-sup  10028  zmax  11823  zbtwnre  11824  supxrunb2  12188  fzrevral  12463  islss4  19010  topbas  20824  elcls3  20935  neips  20965  clslp  21000  subbascn  21106  cnpnei  21116  comppfsc  21383  fgss2  21725  fbflim2  21828  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  metcnp3  22392  aalioulem3  24134  brbtwn2  25830  hial0  28087  hial02  28088  ococss  28280  lnopmi  28987  adjlnop  29073  pjss2coi  29151  pj3cor1i  29196  strlem3a  29239  hstrlem3a  29247  mdbr3  29284  mdbr4  29285  dmdmd  29287  dmdbr3  29292  dmdbr4  29293  dmdbr5  29295  ssmd2  29299  mdslmd1i  29316  mdsymlem7  29396  cdj1i  29420  cdj3lem2b  29424  lub0N  34794  glb0N  34798  hlrelat2  35007  snatpsubN  35354  pmaple  35365  pclclN  35495  pclfinN  35504  pclfinclN  35554  ltrneq2  35752  trlval2  35768  trlord  36174  trintALT  39431  lindslinindsimp2  42577