Theorem ralrimdv 3133

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3051

This theorem is referenced by:  ralrimdva  3135  ralrimivv  3176  wefrc  5617  oneqmin  7745  nneneq  9132  cflm  10162  coflim  10173  isf32lem12  10276  axdc3lem2  10363  zorn2lem7  10414  axpre-sup  11082  zmax  12860  zbtwnre  12861  supxrunb2  13237  fzrevral  13530  lcmfdvdsb  16572  islss4  20915  topbas  22918  elcls3  23029  neips  23059  clslp  23094  subbascn  23200  cnpnei  23210  comppfsc  23478  fgss2  23820  fbflim2  23923  alexsubALTlem3  23995  alexsubALTlem4  23996  alexsubALT  23997  metcnp3  24486  mpomulcn  24816  aalioulem3  26300  onsfi  28334  brbtwn2  28959  hial0  31158  hial02  31159  ococss  31349  lnopmi  32056  adjlnop  32142  pjss2coi  32220  pj3cor1i  32265  strlem3a  32308  hstrlem3a  32316  mdbr3  32353  mdbr4  32354  dmdmd  32356  dmdbr3  32361  dmdbr4  32362  dmdbr5  32364  ssmd2  32368  mdslmd1i  32385  mdsymlem7  32465  cdj1i  32489  cdj3lem2b  32493  rankfilimb  35237  sat1el2xp  35552  fvineqsneu  37585  lub0N  39484  glb0N  39488  hlrelat2  39698  snatpsubN  40045  pclclN  40186  pclfinN  40195  pclfinclN  40245  ltrneq2  40443  trlval2  40458  trlord  40864  trintALT  45158  lindslinindsimp2  48746