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  2486  2eu6  2682  rgen2a  3357  rexraleqim  3601  elreldm  5917  onminex  7814  rntpos  8249  smores  8353  seqomlem2  8454  f1domg  8991  php  9215  fodomnum  10129  carduniima  10168  cardmin  10641  negn0  11738  sqrmo  15411  isch3  31836  cgrtriv  36747  axtco2  37242  dfttc4lem2  37297  wl-lem-moexsb  38480  grpomndo  38789  elghomlem2OLD  38800  tz6.12c-afv2  48281