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

Theorem mpisyl 1446
Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)
Hypotheses
Ref Expression
mpisyl.1  |-  ( ph  ->  ps )
mpisyl.2  |-  ch
mpisyl.3  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
mpisyl  |-  ( ph  ->  th )

Proof of Theorem mpisyl
StepHypRef Expression
1 mpisyl.1 . 2  |-  ( ph  ->  ps )
2 mpisyl.2 . . 3  |-  ch
3 mpisyl.3 . . 3  |-  ( ps 
->  ( ch  ->  th )
)
42, 3mpi 15 . 2  |-  ( ps 
->  th )
51, 4syl 14 1  |-  ( ph  ->  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:  ceqsex  2777  reusv1  4460  fliftcnv  5798  fliftfun  5799  tfrlemibfn  6331  tfr1onlembfn  6347  tfrcllembfn  6360  cnvct  6811  ordiso  7037  exmidomni  7142  djudoml  7220  djudomr  7221  uzsinds  10444  fimaxq  10809  ltoddhalfle  11900  phicl2  12216  strsetsid  12497  txdis1cn  13817  xmeter  13975  subctctexmid  14789
  Copyright terms: Public domain W3C validator