Theorem mpisyl 1492

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  2854  reusv1  4581  iotaexab  5333  fliftcnv  5970  fliftfun  5971  tfrlemibfn  6561  tfr1onlembfn  6577  tfrcllembfn  6590  cnvct  7052  ssfiexmidt  7135  ordiso  7329  exmidomni  7435  djudoml  7528  djudomr  7529  uzsinds  10813  fimaxq  11202  ltoddhalfle  12587  phicl2  12919  strsetsid  13266  txdis1cn  15192  xmeter  15350  2lgslem1  16013  usgredg2v  16268  1loopgrvd2fi  16349  subctctexmid  16823