Theorem mpisyl 1467

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

Step	Hyp	Ref	Expression
1		mpisyl.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpisyl.2	. . 3 ⊢ 𝜒
3		mpisyl.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	2, 3	mpi 15	. 2 ⊢ (𝜓 → 𝜃)
5	1, 4	syl 14	1 ⊢ (𝜑 → 𝜃)

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  2811  reusv1  4509  iotaexab  5255  fliftcnv  5871  fliftfun  5872  tfrlemibfn  6421  tfr1onlembfn  6437  tfrcllembfn  6450  cnvct  6908  ordiso  7145  exmidomni  7251  djudoml  7338  djudomr  7339  uzsinds  10596  fimaxq  10979  ltoddhalfle  12248  phicl2  12580  strsetsid  12909  txdis1cn  14794  xmeter  14952  2lgslem1  15612  subctctexmid  16011