Theorem ralrimdv 3105

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3069

This theorem is referenced by:  ralrimdva  3106  ralrimivv  3122  wefrc  5583  oneqmin  7650  nneneq  8992  nneneqOLD  9004  cflm  10006  coflim  10017  isf32lem12  10120  axdc3lem2  10207  zorn2lem7  10258  axpre-sup  10925  zmax  12685  zbtwnre  12686  supxrunb2  13054  fzrevral  13341  lcmfdvdsb  16348  islss4  20224  topbas  22122  elcls3  22234  neips  22264  clslp  22299  subbascn  22405  cnpnei  22415  comppfsc  22683  fgss2  23025  fbflim2  23128  alexsubALTlem3  23200  alexsubALTlem4  23201  alexsubALT  23202  metcnp3  23696  aalioulem3  25494  brbtwn2  27273  hial0  29464  hial02  29465  ococss  29655  lnopmi  30362  adjlnop  30448  pjss2coi  30526  pj3cor1i  30571  strlem3a  30614  hstrlem3a  30622  mdbr3  30659  mdbr4  30660  dmdmd  30662  dmdbr3  30667  dmdbr4  30668  dmdbr5  30670  ssmd2  30674  mdslmd1i  30691  mdsymlem7  30771  cdj1i  30795  cdj3lem2b  30799  sat1el2xp  33341  fvineqsneu  35582  lub0N  37203  glb0N  37207  hlrelat2  37417  snatpsubN  37764  pmaple  37775  pclclN  37905  pclfinN  37914  pclfinclN  37964  ltrneq2  38162  trlval2  38177  trlord  38583  trintALT  42501  lindslinindsimp2  45804