Theorem ralrimdv 3162

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079

This theorem is used by:  ralrimdva  3164  ralrimivv  3205  wefrc  5654  oneqmin  7797  nneneq  9188  cflm  10239  coflim  10251  isf32lem12  10354  axdc3lem2  10441  zorn2lem7  10492  axpre-sup  11160  zmax  12975  zbtwnre  12976  supxrunb2  13352  fzrevral  13647  lcmfdvdsb  16707  islss4  21094  topbas  23140  elcls3  23251  neips  23281  clslp  23316  subbascn  23422  cnpnei  23432  comppfsc  23700  fgss2  24042  fbflim2  24145  alexsubALTlem3  24217  alexsubALTlem4  24218  alexsubALT  24219  metcnp3  24708  mpomulcn  25037  aalioulem3  26508  onsfi  28560  brbtwn2  29266  hial0  31465  hial02  31466  ococss  31656  lnopmi  32363  adjlnop  32449  pjss2coi  32527  pj3cor1i  32572  strlem3a  32615  hstrlem3a  32623  mdbr3  32660  mdbr4  32661  dmdmd  32663  dmdbr3  32668  dmdbr4  32669  dmdbr5  32671  ssmd2  32675  mdslmd1i  32692  mdsymlem7  32772  cdj1i  32796  cdj3lem2b  32800  rankfilimb  35505  sat1el2xp  35879  fvineqsneu  38085  lub0N  39991  glb0N  39995  hlrelat2  40205  snatpsubN  40552  pclclN  40693  pclfinN  40702  pclfinclN  40752  ltrneq2  40950  trlval2  40965  trlord  41371  trintALT  45617  lindslinindsimp2  49271