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

Theorem alimdv 1833
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 1489 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1426 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1406  ax-gen 1408  ax-17 1489
This theorem is referenced by:  2alimdv  1835  moim  2039  ralimdv2  2477  sstr2  3072  reuss2  3324  ssuni  3726  disjss2  3877  disjss1  3880  disjiun  3892  exmidsssnc  4094  soss  4204  alxfr  4350  ssrel  4595  ssrel2  4597  ssrelrel  4607  iotaval  5067  omnimkv  6996
  Copyright terms: Public domain W3C validator