Theorem mpisyl 1422

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  2724  reusv1  4379  fliftcnv  5696  fliftfun  5697  tfrlemibfn  6225  tfr1onlembfn  6241  tfrcllembfn  6254  cnvct  6703  ordiso  6921  exmidomni  7014  djudoml  7075  djudomr  7076  uzsinds  10215  fimaxq  10573  ltoddhalfle  11590  phicl2  11890  strsetsid  11992  txdis1cn  12447  xmeter  12605  subctctexmid  13196