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  10894  fimaxq  11284  ltoddhalfle  12676  phicl2  13012  strsetsid  13434  txdis1cn  15428  xmeter  15586  ppiqub  16212  2lgslem1  16329  usgredg2v  16584  1loopgrvd2fi  16665  subctctexmid  17149  wexmiddiffilem  17162  wexmiddifxy  17165