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 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  ralrimdva  3162  ralrimivv  3203  wefrc  5644  oneqmin  7814  nneneq  9221  cflm  10327  coflim  10339  isf32lem12  10442  axdc3lem2  10529  zorn2lem7  10580  axpre-sup  11254  zmax  13072  zbtwnre  13073  supxrunb2  13450  fzrevral  13746  lcmfdvdsb  16818  islss4  21237  topbas  23290  elcls3  23401  neips  23431  clslp  23466  subbascn  23572  cnpnei  23582  comppfsc  23851  fgss2  24193  fbflim2  24296  alexsubALTlem3  24368  alexsubALTlem4  24369  alexsubALT  24370  metcnp3  24859  mpomulcn  25188  aalioulem3  26661  onsfi  28742  brbtwn2  29483  hial0  31704  hial02  31705  ococss  31895  lnopmi  32602  adjlnop  32688  pjss2coi  32766  pj3cor1i  32811  strlem3a  32854  hstrlem3a  32862  mdbr3  32899  mdbr4  32900  dmdmd  32902  dmdbr3  32907  dmdbr4  32908  dmdbr5  32910  ssmd2  32914  mdslmd1i  32931  mdsymlem7  33011  cdj1i  33035  cdj3lem2b  33039  rankfilimb  35728  sat1el2xp  36144  fvineqsneu  38335  lub0N  40247  glb0N  40251  hlrelat2  40461  snatpsubN  40808  pclclN  40949  pclfinN  40958  pclfinclN  41008  ltrneq2  41206  trlval2  41221  trlord  41627  trintALT  45863  lindslinindsimp2  49575