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

Theorem mpsyl 65
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 62 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  relcnvtr  5028  relresfld  5038  relcoi1  5040  funco  5133  foimacnv  5353  fvi  5446  isoini2  5688  ovidig  5856  smores2  6159  tfrlem5  6179  snnen2og  6721  phpm  6727  fict  6730  infnfi  6757  isinfinf  6759  exmidpw  6770  difinfinf  6954  enumct  6968  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  isumz  11126  fsumsersdc  11132  isumclim  11158  isumclim3  11160  alzdvds  11479  zsupcl  11567  infssuzex  11569  gcddvds  11579  dvdslegcd  11580  ennnfonelemrn  11859  ctinf  11870  strle1g  11976  metrest  12602  dvef  12783  nnsf  13126  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator