Theorem mpisyl 1446

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  2776  reusv1  4459  fliftcnv  5796  fliftfun  5797  tfrlemibfn  6329  tfr1onlembfn  6345  tfrcllembfn  6358  cnvct  6809  ordiso  7035  exmidomni  7140  djudoml  7218  djudomr  7219  uzsinds  10442  fimaxq  10807  ltoddhalfle  11898  phicl2  12214  strsetsid  12495  txdis1cn  13781  xmeter  13939  subctctexmid  14753