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 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  snssg  3849  relcnvtr  5307  relresfld  5317  relcoi1  5319  funco  5417  foimacnv  5657  fvi  5760  isoini2  6025  ovidig  6206  smores2  6565  tfrlem5  6585  snnen2og  7160  phpm  7167  fict  7170  infnfi  7199  isinfinf  7201  exmidpw  7215  difinfinf  7441  enumct  7455  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  zsupcl  10666  infssuzex  10668  pfxccatin12lem3  11506  isumz  12158  fsumsersdc  12164  isumclim  12190  isumclim3  12192  zprodap0  12350  alzdvds  12623  bitsfzolem  12723  gcddvds  12742  dvdslegcd  12743  pclemub  13068  ballotfilemfc0  13234  ballotfilemfcc  13235  ennnfonelemj0  13294  ennnfonelemg  13296  ennnfonelemrn  13312  ctinf  13323  strle1g  13462  fnpr2ob  13663  metrest  15609  dvef  15830  umgrnloop2  16404  umgrclwwlkge2  16655  bj-charfunbi  16849  pw1nct  17045  nnsf  17060  exmidsbthrlem  17079