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

Theorem alrimdv 1775
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1987 and 19.21v 1786. (Contributed by NM, 10-Feb-1997.)
Hypothesis
Ref Expression
alrimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
alrimdv  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Distinct variable groups:    ph, x    ps, x
Allowed substitution hint:    ch( x)

Proof of Theorem alrimdv
StepHypRef Expression
1 ax-5 1758 . 2  |-  ( ph  ->  A. x ph )
2 ax-5 1758 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1723 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1669  ax-4 1682  ax-5 1758
This theorem is referenced by:  axc9lem2  2133  axc9lem2OLD  2134  zfpair  4637  fliftfun  6205  isofrlem  6231  funcnvuni  6746  f1oweALT  6777  findcard  7810  findcard2  7811  dfac5lem4  8557  dfac5  8559  zorn2lem4  8929  genpcl  9433  psslinpr  9456  ltaddpr  9459  ltexprlem3  9463  suplem1pr  9477  uzwo  11222  seqf1o  12254  ramcl  14987  alexsubALTlem3  21064  intabssd  36216  frege81  36540  frege95  36554  frege123  36582  frege130  36589  truniALT  36902  ggen31  36911  onfrALTlem2  36912  gen21  36998  gen22  37001  ggen22  37002
  Copyright terms: Public domain W3C validator