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

Theorem alrimdv 1843
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2061 and 19.21v 1854. (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 1826 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-5 1826 . 2 (𝜓 → ∀𝑥𝜓)
3 alrimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3alrimdh 1776 1 (𝜑 → (𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem is referenced by:  ax13lem2  2283  reusv1  4787  zfpair  4826  fliftfun  6440  isofrlem  6468  funcnvuni  6990  f1oweALT  7021  findcard  8062  findcard2  8063  dfac5lem4  8810  dfac5  8812  zorn2lem4  9182  genpcl  9687  psslinpr  9710  ltaddpr  9713  ltexprlem3  9717  suplem1pr  9731  uzwo  11586  seqf1o  12662  ramcl  15520  alexsubALTlem3  21611  intabssd  36759  frege81  37082  frege95  37096  frege123  37124  frege130  37131  truniALT  37596  ggen31  37605  onfrALTlem2  37606  gen21  37689  gen22  37692  ggen22  37693
  Copyright terms: Public domain W3C validator