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:  snssg  3827  relcnvtr  5281  relresfld  5291  relcoi1  5293  funco  5391  foimacnv  5631  fvi  5733  isoini2  5991  ovidig  6170  smores2  6524  tfrlem5  6544  snnen2og  7112  phpm  7119  fict  7122  infnfi  7151  isinfinf  7153  exmidpw  7167  difinfinf  7391  enumct  7405  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  zsupcl  10587  infssuzex  10589  pfxccatin12lem3  11417  isumz  12068  fsumsersdc  12074  isumclim  12100  isumclim3  12102  zprodap0  12260  alzdvds  12533  bitsfzolem  12633  gcddvds  12652  dvdslegcd  12653  pclemub  12978  ennnfonelemj0  13141  ennnfonelemg  13143  ennnfonelemrn  13159  ctinf  13170  strle1g  13308  fnpr2ob  13542  metrest  15358  dvef  15579  umgrnloop2  16133  umgrclwwlkge2  16384  bj-charfunbi  16568  pw1nct  16764  nnsf  16770  exmidsbthrlem  16789