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  2491  2eu6  2687  rgen2a  3363  rexraleqim  3609  elreldm  5928  onminex  7803  rntpos  8237  smores  8341  seqomlem2  8440  f1domg  8970  php  9193  fodomnum  10052  carduniima  10091  cardmin  10558  negn0  11653  sqrmo  15313  isch3  31608  cgrtriv  36506  axtco2  37017  dfttc4lem2  37072  wl-lem-moexsb  38255  grpomndo  38558  elghomlem2OLD  38569  tz6.12c-afv2  48011