Theorem syli 40

Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)

Hypotheses

Ref	Expression
syli.1	⊢ (𝜓 → (𝜑 → 𝜒))
syli.2	⊢ (𝜒 → (𝜑 → 𝜃))

Assertion

Ref	Expression
syli	⊢ (𝜓 → (𝜑 → 𝜃))

Proof of Theorem syli

Step	Hyp	Ref	Expression
1		syli.1	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
2		syli.2	. . 3 ⊢ (𝜒 → (𝜑 → 𝜃))
3	2	com12 33	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	sylcom 31	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:  ibd  272  bija  383  equvel  2490  2eu6  2686  rgen2a  3362  rexraleqim  3608  elreldm  5927  onminex  7803  rntpos  8237  smores  8341  seqomlem2  8440  f1domg  8970  php  9194  fodomnum  10053  carduniima  10092  cardmin  10559  negn0  11654  sqrmo  15321  isch3  31622  cgrtriv  36507  axtco2  37018  dfttc4lem2  37073  wl-lem-moexsb  38256  grpomndo  38559  elghomlem2OLD  38570  tz6.12c-afv2  48012