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  2854  reusv1  4584  iotaexab  5336  fliftcnv  5974  fliftfun  5975  tfrlemibfn  6572  tfr1onlembfn  6588  tfrcllembfn  6601  cnvct  7063  ssfiexmidt  7146  ordiso  7340  exmidomni  7446  djudoml  7539  djudomr  7540  uzsinds  10833  fimaxq  11222  ltoddhalfle  12607  phicl2  12939  strsetsid  13332  txdis1cn  15272  xmeter  15430  2lgslem1  16093  usgredg2v  16348  1loopgrvd2fi  16429  subctctexmid  16913