Theorem mpisyl 1469

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  2818  reusv1  4526  iotaexab  5273  fliftcnv  5892  fliftfun  5893  tfrlemibfn  6444  tfr1onlembfn  6460  tfrcllembfn  6473  cnvct  6932  ordiso  7171  exmidomni  7277  djudoml  7369  djudomr  7370  uzsinds  10633  fimaxq  11016  ltoddhalfle  12370  phicl2  12702  strsetsid  13031  txdis1cn  14917  xmeter  15075  2lgslem1  15735  usgredg2v  15987  subctctexmid  16277