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  4550  iotaexab  5300  fliftcnv  5928  fliftfun  5929  tfrlemibfn  6485  tfr1onlembfn  6501  tfrcllembfn  6514  cnvct  6975  ordiso  7219  exmidomni  7325  djudoml  7417  djudomr  7418  uzsinds  10683  fimaxq  11067  ltoddhalfle  12425  phicl2  12757  strsetsid  13086  txdis1cn  14973  xmeter  15131  2lgslem1  15791  usgredg2v  16043  subctctexmid  16479