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  2485  2eu6  2681  rgen2a  3356  rexraleqim  3601  elreldm  5919  onminex  7801  rntpos  8237  smores  8341  seqomlem2  8440  f1domg  8977  php  9201  fodomnum  10060  carduniima  10099  cardmin  10572  negn0  11667  sqrmo  15338  isch3  31722  cgrtriv  36582  axtco2  37093  dfttc4lem2  37148  wl-lem-moexsb  38331  grpomndo  38625  elghomlem2OLD  38636  tz6.12c-afv2  48130