Theorem ralrimdv 3166

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

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

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 3083

This theorem is used by:  ralrimdva  3168  ralrimivv  3209  wefrc  5660  oneqmin  7808  nneneq  9200  cflm  10251  coflim  10263  isf32lem12  10366  axdc3lem2  10453  zorn2lem7  10504  axpre-sup  11172  zmax  12987  zbtwnre  12988  supxrunb2  13364  fzrevral  13659  lcmfdvdsb  16726  islss4  21120  topbas  23166  elcls3  23277  neips  23307  clslp  23342  subbascn  23448  cnpnei  23458  comppfsc  23726  fgss2  24068  fbflim2  24171  alexsubALTlem3  24243  alexsubALTlem4  24244  alexsubALT  24245  metcnp3  24734  mpomulcn  25063  aalioulem3  26534  onsfi  28586  brbtwn2  29292  hial0  31491  hial02  31492  ococss  31682  lnopmi  32389  adjlnop  32475  pjss2coi  32553  pj3cor1i  32598  strlem3a  32641  hstrlem3a  32649  mdbr3  32686  mdbr4  32687  dmdmd  32689  dmdbr3  32694  dmdbr4  32695  dmdbr5  32697  ssmd2  32701  mdslmd1i  32718  mdsymlem7  32798  cdj1i  32822  cdj3lem2b  32826  rankfilimb  35520  sat1el2xp  35891  fvineqsneu  38097  lub0N  40003  glb0N  40007  hlrelat2  40217  snatpsubN  40564  pclclN  40705  pclfinN  40714  pclfinclN  40764  ltrneq2  40962  trlval2  40977  trlord  41383  trintALT  45629  lindslinindsimp2  49283