ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpisyl GIF 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 (𝜑𝜓)
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  2775  reusv1  4458  fliftcnv  5795  fliftfun  5796  tfrlemibfn  6328  tfr1onlembfn  6344  tfrcllembfn  6357  cnvct  6808  ordiso  7034  exmidomni  7139  djudoml  7217  djudomr  7218  uzsinds  10439  fimaxq  10802  ltoddhalfle  11892  phicl2  12208  strsetsid  12489  txdis1cn  13671  xmeter  13829  subctctexmid  14632
  Copyright terms: Public domain W3C validator