Theorem mpisyl 1439

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  2768  reusv1  4443  fliftcnv  5774  fliftfun  5775  tfrlemibfn  6307  tfr1onlembfn  6323  tfrcllembfn  6336  cnvct  6787  ordiso  7013  exmidomni  7118  djudoml  7196  djudomr  7197  uzsinds  10398  fimaxq  10762  ltoddhalfle  11852  phicl2  12168  strsetsid  12449  txdis1cn  13072  xmeter  13230  subctctexmid  14034