Theorem syli 39

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 32	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	sylcom 30	1 ⊢ (𝜓 → (𝜑 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  ibd  269  bija  380  equvel  2460  2eu6  2657  rgen2a  3341  rexraleqim  3601  elreldm  5884  onminex  7747  rntpos  8181  smores  8284  seqomlem2  8382  f1domg  8908  php  9131  fodomnum  9967  carduniima  10006  cardmin  10474  negn0  11566  sqrmo  15174  isch3  31316  cgrtriv  36196  bj-axnul  37276  wl-lem-moexsb  37773  grpomndo  38076  elghomlem2OLD  38087  tz6.12c-afv2  47488