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

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  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