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

Theorem mpsyl 63
Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
Hypotheses
Ref Expression
mpsyl.1  |-  ph
mpsyl.2  |-  ( ps 
->  ch )
mpsyl.3  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
mpsyl  |-  ( ps 
->  th )

Proof of Theorem mpsyl
StepHypRef Expression
1 mpsyl.1 . . 3  |-  ph
21a1i 9 . 2  |-  ( ps 
->  ph )
3 mpsyl.2 . 2  |-  ( ps 
->  ch )
4 mpsyl.3 . 2  |-  ( ph  ->  ( ch  ->  th )
)
52, 3, 4sylc 60 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  relcnvtr  4865  relresfld  4872  relcoi1  4874  funco  4965  foimacnv  5169  fvi  5255  isoini2  5483  ovidig  5643  smores2  5937  tfrlem5  5958  snnen2og  6350  phpm  6355  cauappcvgprlemm  6771  caucvgprlemm  6794  caucvgprprlemml  6820  caucvgsr  6914  alzdvds  10129
  Copyright terms: Public domain W3C validator