MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alrimdv Structured version   Visualization version   GIF version

Theorem alrimdv 1930
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2208 and 19.21v 1940. (Contributed by NM, 10-Feb-1997.)
Hypothesis
Ref Expression
alrimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
alrimdv (𝜑 → (𝜓 → ∀𝑥𝜒))
Distinct variable groups:   𝜑,𝑥   𝜓,𝑥
Allowed substitution hint:   𝜒(𝑥)

Proof of Theorem alrimdv
StepHypRef Expression
1 ax-5 1911 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-5 1911 . 2 (𝜓 → ∀𝑥𝜓)
3 alrimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3alrimdh 1864 1 (𝜑 → (𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem is referenced by:  sbequ1  2250  ax13lem2  2395  reusv1  5275  zfpair  5299  fliftfun  7049  isofrlem  7077  funcnvuni  7622  f1oweALT  7659  findcard  8745  findcard2  8746  dfac5lem4  9541  dfac5  9543  zorn2lem4  9910  genpcl  10419  psslinpr  10442  ltaddpr  10445  ltexprlem3  10449  suplem1pr  10463  uzwo  12299  seqf1o  13407  ramcl  16354  alexsubALTlem3  22652  bj-dvelimdv1  34252  intabssd  40157  frege81  40576  frege95  40590  frege123  40618  frege130  40625  truniALT  41181  ggen31  41185  onfrALTlem2  41186  gen21  41259  gen22  41262  ggen22  41263
  Copyright terms: Public domain W3C validator