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  2851  reusv1  4578  iotaexab  5330  fliftcnv  5967  fliftfun  5968  tfrlemibfn  6558  tfr1onlembfn  6574  tfrcllembfn  6587  cnvct  7049  ssfiexmidt  7132  ordiso  7326  exmidomni  7432  djudoml  7525  djudomr  7526  uzsinds  10802  fimaxq  11187  ltoddhalfle  12572  phicl2  12904  strsetsid  13234  txdis1cn  15130  xmeter  15288  2lgslem1  15951  usgredg2v  16206  1loopgrvd2fi  16287  subctctexmid  16761