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

Theorem mpsyl 64
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 61 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  4870  relresfld  4877  relcoi1  4879  funco  4970  foimacnv  5175  fvi  5262  isoini2  5489  ovidig  5649  smores2  5943  tfrlem5  5963  snnen2og  6394  phpm  6400  fict  6403  infnfi  6429  cauappcvgprlemm  6897  caucvgprlemm  6920  caucvgprprlemml  6946  caucvgsr  7040  alzdvds  10399  zsupcl  10487  infssuzex  10489  gcddvds  10499  dvdslegcd  10500
  Copyright terms: Public domain W3C validator