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 2198 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 1537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1911
This theorem is referenced by:  sbequ1  2238  ax13lem2  2373  reusv1  5394  zfpair  5418  fliftfun  7311  isofrlem  7339  funcnvuni  7924  f1oweALT  7961  findcard  9165  findcard2  9166  findcard2OLD  9286  dfac5lem4  10123  dfac5  10125  zorn2lem4  10496  genpcl  11005  psslinpr  11028  ltaddpr  11031  ltexprlem3  11035  suplem1pr  11049  uzwo  12899  seqf1o  14013  ramcl  16966  alexsubALTlem3  23773  bj-dvelimdv1  36034  intabssd  42572  frege81  42997  frege95  43011  frege123  43039  frege130  43046  truniALT  43604  ggen31  43608  onfrALTlem2  43609  gen21  43682  gen22  43685  ggen22  43686
  Copyright terms: Public domain W3C validator