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  2775  reusv1  4458  fliftcnv  5795  fliftfun  5796  tfrlemibfn  6328  tfr1onlembfn  6344  tfrcllembfn  6357  cnvct  6808  ordiso  7034  exmidomni  7139  djudoml  7217  djudomr  7218  uzsinds  10441  fimaxq  10806  ltoddhalfle  11897  phicl2  12213  strsetsid  12494  txdis1cn  13748  xmeter  13906  subctctexmid  14720