ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  alimdv Unicode version

Theorem alimdv 1872
Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
alimdv  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem alimdv
StepHypRef Expression
1 ax-17 1519 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1460 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1440  ax-gen 1442  ax-17 1519
This theorem is referenced by:  2alimdv  1874  moim  2083  ralimdv2  2540  sstr2  3154  reuss2  3407  ssuni  3816  disjss2  3967  disjss1  3970  disjiun  3982  exmidsssnc  4187  soss  4297  alxfr  4444  ssrel  4697  ssrel2  4699  ssrelrel  4709  iotaval  5169  omnimkv  7130
  Copyright terms: Public domain W3C validator