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  2841  reusv1  4555  iotaexab  5305  fliftcnv  5936  fliftfun  5937  tfrlemibfn  6494  tfr1onlembfn  6510  tfrcllembfn  6523  cnvct  6984  ssfiexmidt  7065  ordiso  7235  exmidomni  7341  djudoml  7434  djudomr  7435  uzsinds  10707  fimaxq  11092  ltoddhalfle  12456  phicl2  12788  strsetsid  13117  txdis1cn  15005  xmeter  15163  2lgslem1  15823  usgredg2v  16078  1loopgrvd2fi  16159  subctctexmid  16622