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  5310  relresfld  5320  relcoi1  5322  funco  5420  foimacnv  5660  fvi  5763  isoini2  6028  ovidig  6209  smores2  6569  tfrlem5  6589  snnen2og  7165  phpm  7172  fict  7175  infnfi  7204  isinfinf  7206  exmidpw  7220  difinfinf  7448  enumct  7462  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  zsupcl  10682  infssuzex  10684  pfxccatin12lem3  11527  isumz  12182  fsumsersdc  12188  isumclim  12214  isumclim3  12216  zprodap0  12374  alzdvds  12647  bitsfzolem  12747  gcddvds  12766  dvdslegcd  12767  pclemub  13096  ballotfilemfc0  13291  ballotfilemfcc  13292  ennnfonelemj0  13351  ennnfonelemg  13353  ennnfonelemrn  13369  ctinf  13380  strle1g  13520  fnpr2ob  13721  metrest  15744  dvef  15965  umgrnloop2  16609  umgrclwwlkge2  16860  bj-charfunbi  17054  pw1nct  17250  nnsf  17266  exmidsbthrlem  17285