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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  ∀wral 3078

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  ralrimdva  3164  ralrimivv  3205  wefrc  5643  oneqmin  7785  nneneq  9176  cflm  10208  coflim  10220  isf32lem12  10323  axdc3lem2  10410  zorn2lem7  10461  axpre-sup  11129  zmax  12948  zbtwnre  12949  supxrunb2  13325  fzrevral  13619  lcmfdvdsb  16679  islss4  21031  topbas  23034  elcls3  23145  neips  23175  clslp  23210  subbascn  23316  cnpnei  23326  comppfsc  23594  fgss2  23936  fbflim2  24039  alexsubALTlem3  24111  alexsubALTlem4  24112  alexsubALT  24113  metcnp3  24602  mpomulcn  24931  aalioulem3  26400  onsfi  28451  brbtwn2  29108  hial0  31307  hial02  31308  ococss  31498  lnopmi  32205  adjlnop  32291  pjss2coi  32369  pj3cor1i  32414  strlem3a  32457  hstrlem3a  32465  mdbr3  32502  mdbr4  32503  dmdmd  32505  dmdbr3  32510  dmdbr4  32511  dmdbr5  32513  ssmd2  32517  mdslmd1i  32534  mdsymlem7  32614  cdj1i  32638  cdj3lem2b  32642  rankfilimb  35402  sat1el2xp  35734  fvineqsneu  37910  lub0N  39818  glb0N  39822  hlrelat2  40032  snatpsubN  40379  pclclN  40520  pclfinN  40529  pclfinclN  40579  ltrneq2  40777  trlval2  40792  trlord  41198  trintALT  45461  lindslinindsimp2  49090