Theorem mpisyl 1496

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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  ceqsex  2860  reusv1  4604  iotaexab  5356  fliftcnv  6001  fliftfun  6002  tfrlemibfn  6599  tfr1onlembfn  6615  tfrcllembfn  6628  cnvct  7097  ssfiexmidt  7180  ordiso  7376  exmidomni  7482  djudoml  7575  djudomr  7576  uzsinds  10883  fimaxq  11272  ltoddhalfle  12662  phicl2  12994  strsetsid  13387  txdis1cn  15381  xmeter  15539  2lgslem1  16222  usgredg2v  16477  1loopgrvd2fi  16558  subctctexmid  17042  wexmiddiffilem  17055  wexmiddifxy  17058