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

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  2860  reusv1  4602  iotaexab  5354  fliftcnv  5995  fliftfun  5996  tfrlemibfn  6593  tfr1onlembfn  6609  tfrcllembfn  6622  cnvct  7091  ssfiexmidt  7174  ordiso  7370  exmidomni  7476  djudoml  7569  djudomr  7570  uzsinds  10864  fimaxq  11253  ltoddhalfle  12643  phicl2  12975  strsetsid  13368  txdis1cn  15362  xmeter  15520  2lgslem1  16193  usgredg2v  16448  1loopgrvd2fi  16529  subctctexmid  17013