Theorem mpisyl 1457

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  2801  reusv1  4494  iotaexab  5238  fliftcnv  5845  fliftfun  5846  tfrlemibfn  6395  tfr1onlembfn  6411  tfrcllembfn  6424  cnvct  6877  ordiso  7111  exmidomni  7217  djudoml  7304  djudomr  7305  uzsinds  10555  fimaxq  10938  ltoddhalfle  12077  phicl2  12409  strsetsid  12738  txdis1cn  14600  xmeter  14758  2lgslem1  15418  subctctexmid  15733