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

Theorem alrimdv 1933
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2201 and 19.21v 1943. (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 1914 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-5 1914 . 2 (𝜓 → ∀𝑥𝜓)
3 alrimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3alrimdh 1867 1 (𝜑 → (𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem is referenced by:  sbequ1  2241  ax13lem2  2376  reusv1  5391  zfpair  5415  fliftfun  7296  isofrlem  7324  funcnvuni  7909  f1oweALT  7946  findcard  9151  findcard2  9152  findcard2OLD  9272  dfac5lem4  10108  dfac5  10110  zorn2lem4  10481  genpcl  10990  psslinpr  11013  ltaddpr  11016  ltexprlem3  11020  suplem1pr  11034  uzwo  12882  seqf1o  13996  ramcl  16949  alexsubALTlem3  23522  bj-dvelimdv1  35636  intabssd  42141  frege81  42566  frege95  42580  frege123  42608  frege130  42615  truniALT  43173  ggen31  43177  onfrALTlem2  43178  gen21  43251  gen22  43254  ggen22  43255
  Copyright terms: Public domain W3C validator