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  3847  relcnvtr  5305  relresfld  5315  relcoi1  5317  funco  5415  foimacnv  5655  fvi  5757  isoini2  6019  ovidig  6200  smores2  6559  tfrlem5  6579  snnen2og  7154  phpm  7161  fict  7164  infnfi  7193  isinfinf  7195  exmidpw  7209  difinfinf  7435  enumct  7449  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  zsupcl  10647  infssuzex  10649  pfxccatin12lem3  11487  isumz  12139  fsumsersdc  12145  isumclim  12171  isumclim3  12173  zprodap0  12331  alzdvds  12604  bitsfzolem  12704  gcddvds  12723  dvdslegcd  12724  pclemub  13049  ballotfilemfc0  13215  ballotfilemfcc  13216  ennnfonelemj0  13275  ennnfonelemg  13277  ennnfonelemrn  13293  ctinf  13304  strle1g  13443  fnpr2ob  13644  metrest  15590  dvef  15811  umgrnloop2  16375  umgrclwwlkge2  16626  bj-charfunbi  16820  pw1nct  17016  nnsf  17022  exmidsbthrlem  17041