Theorem mpisyl 1491

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  2840  reusv1  4557  iotaexab  5307  fliftcnv  5941  fliftfun  5942  tfrlemibfn  6499  tfr1onlembfn  6515  tfrcllembfn  6528  cnvct  6989  ssfiexmidt  7070  ordiso  7240  exmidomni  7346  djudoml  7439  djudomr  7440  uzsinds  10712  fimaxq  11097  ltoddhalfle  12477  phicl2  12809  strsetsid  13138  txdis1cn  15031  xmeter  15189  2lgslem1  15849  usgredg2v  16104  1loopgrvd2fi  16185  subctctexmid  16661