Theorem mpisyl 1489

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  2838  reusv1  4549  iotaexab  5297  fliftcnv  5925  fliftfun  5926  tfrlemibfn  6480  tfr1onlembfn  6496  tfrcllembfn  6509  cnvct  6970  ordiso  7211  exmidomni  7317  djudoml  7409  djudomr  7410  uzsinds  10674  fimaxq  11057  ltoddhalfle  12412  phicl2  12744  strsetsid  13073  txdis1cn  14960  xmeter  15118  2lgslem1  15778  usgredg2v  16030  subctctexmid  16395