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  3833  relcnvtr  5287  relresfld  5297  relcoi1  5299  funco  5397  foimacnv  5637  fvi  5739  isoini2  5998  ovidig  6179  smores2  6538  tfrlem5  6558  snnen2og  7126  phpm  7133  fict  7136  infnfi  7165  isinfinf  7167  exmidpw  7181  difinfinf  7405  enumct  7419  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  zsupcl  10616  infssuzex  10618  pfxccatin12lem3  11452  isumz  12103  fsumsersdc  12109  isumclim  12135  isumclim3  12137  zprodap0  12295  alzdvds  12568  bitsfzolem  12668  gcddvds  12687  dvdslegcd  12688  pclemub  13013  ballotfilemfc0  13179  ballotfilemfcc  13180  ennnfonelemj0  13239  ennnfonelemg  13241  ennnfonelemrn  13257  ctinf  13268  strle1g  13406  fnpr2ob  13607  metrest  15500  dvef  15721  umgrnloop2  16275  umgrclwwlkge2  16526  bj-charfunbi  16720  pw1nct  16916  nnsf  16922  exmidsbthrlem  16941