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  3756  relcnvtr  5189  relresfld  5199  relcoi1  5201  funco  5298  foimacnv  5522  fvi  5618  isoini2  5866  ovidig  6040  smores2  6352  tfrlem5  6372  snnen2og  6920  phpm  6926  fict  6929  infnfi  6956  isinfinf  6958  exmidpw  6969  difinfinf  7167  enumct  7181  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  zsupcl  10321  infssuzex  10323  isumz  11554  fsumsersdc  11560  isumclim  11586  isumclim3  11588  zprodap0  11746  alzdvds  12019  bitsfzolem  12118  gcddvds  12130  dvdslegcd  12131  pclemub  12456  ennnfonelemj0  12618  ennnfonelemg  12620  ennnfonelemrn  12636  ctinf  12647  strle1g  12784  fnpr2ob  12983  metrest  14742  dvef  14963  bj-charfunbi  15457  pw1nct  15647  nnsf  15649  exmidsbthrlem  15666