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

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  2775  reusv1  4456  fliftcnv  5791  fliftfun  5792  tfrlemibfn  6324  tfr1onlembfn  6340  tfrcllembfn  6353  cnvct  6804  ordiso  7030  exmidomni  7135  djudoml  7213  djudomr  7214  uzsinds  10435  fimaxq  10798  ltoddhalfle  11888  phicl2  12204  strsetsid  12485  txdis1cn  13560  xmeter  13718  subctctexmid  14521