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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  relcnvtr  4994  relresfld  5004  relcoi1  5006  funco  5099  foimacnv  5319  fvi  5410  isoini2  5652  ovidig  5820  smores2  6121  tfrlem5  6141  snnen2og  6682  phpm  6688  fict  6691  infnfi  6718  isinfinf  6720  exmidpw  6731  difinfinf  6901  enumct  6914  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  isumz  10997  fsumsersdc  11003  isumclim  11029  isumclim3  11031  alzdvds  11347  zsupcl  11435  infssuzex  11437  gcddvds  11447  dvdslegcd  11448  ennnfonelemrn  11724  ctinf  11735  strle1g  11831  metrest  12434  nnsf  12783  exmidsbthrlem  12801
  Copyright terms: Public domain W3C validator