Theorem mpsyl 65

Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

Ref	Expression
mpsyl.1	⊢ 𝜑
mpsyl.2	⊢ (𝜓 → 𝜒)
mpsyl.3	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
mpsyl	⊢ (𝜓 → 𝜃)

Proof of Theorem mpsyl

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3 ⊢ 𝜑
2	1	a1i 9	. 2 ⊢ (𝜓 → 𝜑)
3		mpsyl.2	. 2 ⊢ (𝜓 → 𝜒)
4		mpsyl.3	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	2, 3, 4	sylc 62	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  relcnvtr  5016  relresfld  5026  relcoi1  5028  funco  5121  foimacnv  5341  fvi  5432  isoini2  5674  ovidig  5842  smores2  6145  tfrlem5  6165  snnen2og  6706  phpm  6712  fict  6715  infnfi  6742  isinfinf  6744  exmidpw  6755  difinfinf  6938  enumct  6952  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  isumz  11050  fsumsersdc  11056  isumclim  11082  isumclim3  11084  alzdvds  11400  zsupcl  11488  infssuzex  11490  gcddvds  11500  dvdslegcd  11501  ennnfonelemrn  11777  ctinf  11788  strle1g  11892  metrest  12495  nnsf  12891  exmidsbthrlem  12909