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

Theorem alrimdv 2020
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2242 and 19.21v 2031. (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 2001 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-5 2001 . 2 (𝜓 → ∀𝑥𝜓)
3 alrimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3alrimdh 1951 1 (𝜑 → (𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem is referenced by:  ax13lem2  2463  reusv1  5064  zfpair  5092  fliftfun  6784  isofrlem  6812  funcnvuni  7347  f1oweALT  7380  findcard  8436  findcard2  8437  dfac5lem4  9230  dfac5  9232  zorn2lem4  9604  genpcl  10113  psslinpr  10136  ltaddpr  10139  ltexprlem3  10143  suplem1pr  10157  uzwo  11968  seqf1o  13063  ramcl  15948  alexsubALTlem3  22064  bj-dvelimdv1  33145  intabssd  38414  frege81  38736  frege95  38750  frege123  38778  frege130  38785  truniALT  39247  ggen31  39256  onfrALTlem2  39257  gen21  39340  gen22  39343  ggen22  39344
  Copyright terms: Public domain W3C validator