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  4606  iotaexab  5359  fliftcnv  6004  fliftfun  6005  tfrlemibfn  6603  tfr1onlembfn  6619  tfrcllembfn  6632  cnvct  7102  ssfiexmidt  7185  ordiso  7383  exmidomni  7489  djudoml  7582  djudomr  7583  uzsinds  10903  fimaxq  11293  ltoddhalfle  12686  phicl2  13022  strsetsid  13444  txdis1cn  15516  xmeter  15674  ppiqub  16305  2lgslem1  16427  usgredg2v  16682  1loopgrvd2fi  16763  subctctexmid  17247  wexmiddiffilem  17260  wexmiddifxy  17263