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

Theorem alrimdv 1928
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2206 and 19.21v 1938. (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 1909 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-5 1909 . 2 (𝜓 → ∀𝑥𝜓)
3 alrimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3alrimdh 1862 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 1794  ax-4 1808  ax-5 1909
This theorem is referenced by:  sbequ1  2247  ax13lem2  2380  reusv1  5396  zfpair  5420  axprlem3  5424  fliftfun  7333  isofrlem  7361  funcnvuni  7955  f1oweALT  7998  findcard  9204  findcard2  9205  dfac5lem4  10167  dfac5lem4OLD  10169  dfac5  10170  zorn2lem4  10540  genpcl  11049  psslinpr  11072  ltaddpr  11075  ltexprlem3  11079  suplem1pr  11093  uzwo  12954  seqf1o  14085  ramcl  17068  alexsubALTlem3  24058  bj-dvelimdv1  36854  intabssd  43537  frege81  43962  frege95  43976  frege123  44004  frege130  44011  truniALT  44566  ggen31  44570  onfrALTlem2  44571  gen21  44644  gen22  44647  ggen22  44648  relpfrlem  44979
  Copyright terms: Public domain W3C validator