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  4916  relresfld  4926  relcoi1  4928  funco  5019  foimacnv  5234  fvi  5324  isoini2  5559  ovidig  5719  smores2  6013  tfrlem5  6033  snnen2og  6527  phpm  6533  fict  6536  infnfi  6563  isinfinf  6565  exmidpw  6576  djuun  6704  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  isumz  10669  fisumsers  10675  alzdvds  10737  zsupcl  10825  infssuzex  10827  gcddvds  10837  dvdslegcd  10838  nnsf  11340  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator