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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  relcnvtr  5104  relresfld  5114  relcoi1  5116  funco  5209  foimacnv  5431  fvi  5524  isoini2  5766  ovidig  5935  smores2  6238  tfrlem5  6258  snnen2og  6801  phpm  6807  fict  6810  infnfi  6837  isinfinf  6839  exmidpw  6850  difinfinf  7039  enumct  7053  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  isumz  11279  fsumsersdc  11285  isumclim  11311  isumclim3  11313  zprodap0  11471  alzdvds  11738  zsupcl  11826  infssuzex  11828  gcddvds  11838  dvdslegcd  11839  ennnfonelemrn  12131  ctinf  12142  strle1g  12251  metrest  12877  dvef  13059  bj-charfunbi  13357  pw1nct  13546  nnsf  13548  exmidsbthrlem  13564