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

Theorem mpisyl 1405
 Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)
Hypotheses
Ref Expression
mpisyl.1 (𝜑𝜓)
mpisyl.2 𝜒
mpisyl.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
mpisyl (𝜑𝜃)

Proof of Theorem mpisyl
StepHypRef Expression
1 mpisyl.1 . 2 (𝜑𝜓)
2 mpisyl.2 . . 3 𝜒
3 mpisyl.3 . . 3 (𝜓 → (𝜒𝜃))
42, 3mpi 15 . 2 (𝜓𝜃)
51, 4syl 14 1 (𝜑𝜃)
 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  2696  reusv1  4347  fliftcnv  5662  fliftfun  5663  tfrlemibfn  6191  tfr1onlembfn  6207  tfrcllembfn  6220  cnvct  6669  ordiso  6887  exmidomni  6980  djudoml  7039  djudomr  7040  uzsinds  10166  fimaxq  10524  ltoddhalfle  11497  phicl2  11796  strsetsid  11898  txdis1cn  12353  xmeter  12511  subctctexmid  13030
 Copyright terms: Public domain W3C validator