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  2488  2eu6  2684  rgen2a  3360  rexraleqim  3604  elreldm  5929  onminex  7850  rntpos  8294  smores  8398  seqomlem2  8499  f1domg  9036  php  9260  fodomnum  10175  carduniima  10214  cardmin  10687  negn0  11784  sqrmo  15461  isch3  31900  acwer1prclem  35892  onprcf1acwevdlem1  36086  cgrtriv  36982  axtco2  37477  dfttc4lem2  37532  wl-lem-moexsb  38768  grpomndo  39075  elghomlem2OLD  39086  tz6.12c-afv2  48585