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

Theorem mpisyl 1426
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  2750  reusv1  4418  fliftcnv  5745  fliftfun  5746  tfrlemibfn  6275  tfr1onlembfn  6291  tfrcllembfn  6304  cnvct  6754  ordiso  6980  exmidomni  7085  djudoml  7154  djudomr  7155  uzsinds  10341  fimaxq  10701  ltoddhalfle  11783  phicl2  12088  strsetsid  12223  txdis1cn  12678  xmeter  12836  subctctexmid  13573
  Copyright terms: Public domain W3C validator