Theorem ralrimdv 3160

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  ralrimdva  3162  ralrimivv  3203  wefrc  5641  oneqmin  7797  nneneq  9199  cflm  10298  coflim  10310  isf32lem12  10413  axdc3lem2  10500  zorn2lem7  10551  axpre-sup  11225  zmax  13041  zbtwnre  13042  supxrunb2  13419  fzrevral  13714  lcmfdvdsb  16780  islss4  21198  topbas  23251  elcls3  23362  neips  23392  clslp  23427  subbascn  23533  cnpnei  23543  comppfsc  23812  fgss2  24154  fbflim2  24257  alexsubALTlem3  24329  alexsubALTlem4  24330  alexsubALT  24331  metcnp3  24820  mpomulcn  25149  aalioulem3  26624  onsfi  28675  brbtwn2  29416  hial0  31637  hial02  31638  ococss  31828  lnopmi  32535  adjlnop  32621  pjss2coi  32699  pj3cor1i  32744  strlem3a  32787  hstrlem3a  32795  mdbr3  32832  mdbr4  32833  dmdmd  32835  dmdbr3  32840  dmdbr4  32841  dmdbr5  32843  ssmd2  32847  mdslmd1i  32864  mdsymlem7  32944  cdj1i  32968  cdj3lem2b  32972  rankfilimb  35658  sat1el2xp  36065  fvineqsneu  38254  lub0N  40166  glb0N  40170  hlrelat2  40380  snatpsubN  40727  pclclN  40868  pclfinN  40877  pclfinclN  40927  ltrneq2  41125  trlval2  41140  trlord  41546  trintALT  45807  lindslinindsimp2  49497