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  3830  relcnvtr  5284  relresfld  5294  relcoi1  5296  funco  5394  foimacnv  5634  fvi  5736  isoini2  5994  ovidig  6173  smores2  6527  tfrlem5  6547  snnen2og  7115  phpm  7122  fict  7125  infnfi  7154  isinfinf  7156  exmidpw  7170  difinfinf  7394  enumct  7408  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  zsupcl  10598  infssuzex  10600  pfxccatin12lem3  11432  isumz  12083  fsumsersdc  12089  isumclim  12115  isumclim3  12117  zprodap0  12275  alzdvds  12548  bitsfzolem  12648  gcddvds  12667  dvdslegcd  12668  pclemub  12993  ballotfilemfc0  13157  ballotfilemfcc  13158  ennnfonelemj0  13173  ennnfonelemg  13175  ennnfonelemrn  13191  ctinf  13202  strle1g  13340  fnpr2ob  13574  metrest  15420  dvef  15641  umgrnloop2  16195  umgrclwwlkge2  16446  bj-charfunbi  16630  pw1nct  16826  nnsf  16832  exmidsbthrlem  16851