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  2839  reusv1  4553  iotaexab  5303  fliftcnv  5931  fliftfun  5932  tfrlemibfn  6489  tfr1onlembfn  6505  tfrcllembfn  6518  cnvct  6979  ssfiexmidt  7060  ordiso  7229  exmidomni  7335  djudoml  7427  djudomr  7428  uzsinds  10699  fimaxq  11084  ltoddhalfle  12447  phicl2  12779  strsetsid  13108  txdis1cn  14995  xmeter  15153  2lgslem1  15813  usgredg2v  16068  1loopgrvd2fi  16116  subctctexmid  16551