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  7377  exmidomni  7483  djudoml  7576  djudomr  7577  uzsinds  10896  fimaxq  11286  ltoddhalfle  12679  phicl2  13015  strsetsid  13437  txdis1cn  15470  xmeter  15628  ppiqub  16259  2lgslem1  16381  usgredg2v  16636  1loopgrvd2fi  16717  subctctexmid  17201  wexmiddiffilem  17214  wexmiddifxy  17217