Theorem ralrimdv 3139

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  ralrimdva  3141  ralrimivv  3182  wefrc  5615  oneqmin  7747  nneneq  9134  cflm  10167  coflim  10178  isf32lem12  10281  axdc3lem2  10368  zorn2lem7  10419  axpre-sup  11087  zmax  12890  zbtwnre  12891  supxrunb2  13267  fzrevral  13561  lcmfdvdsb  16607  islss4  20956  topbas  22959  elcls3  23070  neips  23100  clslp  23135  subbascn  23241  cnpnei  23251  comppfsc  23519  fgss2  23861  fbflim2  23964  alexsubALTlem3  24036  alexsubALTlem4  24037  alexsubALT  24038  metcnp3  24527  mpomulcn  24856  aalioulem3  26322  onsfi  28370  brbtwn2  28996  hial0  31195  hial02  31196  ococss  31386  lnopmi  32093  adjlnop  32179  pjss2coi  32257  pj3cor1i  32302  strlem3a  32345  hstrlem3a  32353  mdbr3  32390  mdbr4  32391  dmdmd  32393  dmdbr3  32398  dmdbr4  32399  dmdbr5  32401  ssmd2  32405  mdslmd1i  32422  mdsymlem7  32502  cdj1i  32526  cdj3lem2b  32530  rankfilimb  35298  sat1el2xp  35622  fvineqsneu  37788  lub0N  39696  glb0N  39700  hlrelat2  39910  snatpsubN  40257  pclclN  40398  pclfinN  40407  pclfinclN  40457  ltrneq2  40655  trlval2  40670  trlord  41076  trintALT  45339  lindslinindsimp2  48968