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  2454  2eu6  2650  rgen2a  3342  rexraleqim  3610  elreldm  5888  tz6.12cOLD  6867  onminex  7758  rntpos  8195  smores  8298  seqomlem2  8396  f1domg  8920  php  9148  fodomnum  9986  carduniima  10025  cardmin  10493  negn0  11583  sqrmo  15193  isch3  31143  cgrtriv  35963  wl-lem-moexsb  37529  grpomndo  37842  elghomlem2OLD  37853  tz6.12c-afv2  47216