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  3752  relcnvtr  5185  relresfld  5195  relcoi1  5197  funco  5294  foimacnv  5518  fvi  5614  isoini2  5862  ovidig  6036  smores2  6347  tfrlem5  6367  snnen2og  6915  phpm  6921  fict  6924  infnfi  6951  isinfinf  6953  exmidpw  6964  difinfinf  7160  enumct  7174  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  isumz  11532  fsumsersdc  11538  isumclim  11564  isumclim3  11566  zprodap0  11724  alzdvds  11996  zsupcl  12084  infssuzex  12086  gcddvds  12100  dvdslegcd  12101  pclemub  12425  ennnfonelemj0  12558  ennnfonelemg  12560  ennnfonelemrn  12576  ctinf  12587  strle1g  12724  fnpr2ob  12923  metrest  14674  dvef  14873  bj-charfunbi  15303  pw1nct  15493  nnsf  15495  exmidsbthrlem  15512