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

Theorem alrimdv 1726
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1910 and 19.21v 1734. (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 1709 . 2  |-  ( ph  ->  A. x ph )
2 ax-5 1709 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1677 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem is referenced by:  axc9lem2  2044  zfpair  4674  fliftfun  6185  isofrlem  6211  funcnvuni  6726  f1oweALT  6757  findcard  7751  findcard2  7752  dfac5lem4  8498  dfac5  8500  zorn2lem4  8870  genpcl  9375  psslinpr  9398  ltaddpr  9401  ltexprlem3  9405  suplem1pr  9419  uzwo  11145  uzwoOLD  11146  seqf1o  12130  ramcl  14631  alexsubALTlem3  20715  truniALT  33702  ggen31  33711  onfrALTlem2  33712  gen21  33799  gen22  33802  ggen22  33803
  Copyright terms: Public domain W3C validator