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

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

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 3079

This theorem is used by:  ralrimdva  3164  ralrimivv  3205  wefrc  5653  oneqmin  7802  nneneq  9203  cflm  10254  coflim  10266  isf32lem12  10369  axdc3lem2  10456  zorn2lem7  10507  axpre-sup  11181  zmax  12997  zbtwnre  12998  supxrunb2  13374  fzrevral  13669  lcmfdvdsb  16737  islss4  21147  topbas  23198  elcls3  23309  neips  23339  clslp  23374  subbascn  23480  cnpnei  23490  comppfsc  23759  fgss2  24101  fbflim2  24204  alexsubALTlem3  24276  alexsubALTlem4  24277  alexsubALT  24278  metcnp3  24767  mpomulcn  25096  aalioulem3  26567  onsfi  28619  brbtwn2  29348  hial0  31569  hial02  31570  ococss  31760  lnopmi  32467  adjlnop  32553  pjss2coi  32631  pj3cor1i  32676  strlem3a  32719  hstrlem3a  32727  mdbr3  32764  mdbr4  32765  dmdmd  32767  dmdbr3  32772  dmdbr4  32773  dmdbr5  32775  ssmd2  32779  mdslmd1i  32796  mdsymlem7  32876  cdj1i  32900  cdj3lem2b  32904  rankfilimb  35597  sat1el2xp  35945  fvineqsneu  38152  lub0N  40049  glb0N  40053  hlrelat2  40263  snatpsubN  40610  pclclN  40751  pclfinN  40760  pclfinclN  40810  ltrneq2  41008  trlval2  41023  trlord  41429  trintALT  45690  lindslinindsimp2  49380