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

Theorem alrimdv 2009
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2231 and 19.21v 2020. (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 1991 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-5 1991 . 2 (𝜓 → ∀𝑥𝜓)
3 alrimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3alrimdh 1941 1 (𝜑 → (𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem is referenced by:  ax13lem2  2451  reusv1  4998  zfpair  5033  fliftfun  6708  isofrlem  6736  funcnvuni  7270  f1oweALT  7303  findcard  8359  findcard2  8360  dfac5lem4  9153  dfac5  9155  zorn2lem4  9527  genpcl  10036  psslinpr  10059  ltaddpr  10062  ltexprlem3  10066  suplem1pr  10080  uzwo  11959  seqf1o  13049  ramcl  15940  alexsubALTlem3  22073  bj-dvelimdv1  33169  intabssd  38442  frege81  38764  frege95  38778  frege123  38806  frege130  38813  truniALT  39276  ggen31  39285  onfrALTlem2  39286  gen21  39369  gen22  39372  ggen22  39373
  Copyright terms: Public domain W3C validator