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

Theorem alrimdv 2006
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2222 and 19.21v 2017. (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 1988 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-5 1988 . 2 (𝜓 → ∀𝑥𝜓)
3 alrimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3alrimdh 1939 1 (𝜑 → (𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem is referenced by:  ax13lem2  2441  reusv1  5015  zfpair  5053  fliftfun  6726  isofrlem  6754  funcnvuni  7285  f1oweALT  7318  findcard  8366  findcard2  8367  dfac5lem4  9159  dfac5  9161  zorn2lem4  9533  genpcl  10042  psslinpr  10065  ltaddpr  10068  ltexprlem3  10072  suplem1pr  10086  uzwo  11964  seqf1o  13056  ramcl  15955  alexsubALTlem3  22074  bj-dvelimdv1  33162  intabssd  38436  frege81  38758  frege95  38772  frege123  38800  frege130  38807  truniALT  39271  ggen31  39280  onfrALTlem2  39281  gen21  39364  gen22  39367  ggen22  39368
  Copyright terms: Public domain W3C validator