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  271  bija  384  equviniOLD  2478  equvel  2479  2eu6  2742  rgen2a  3231  rexraleqim  3642  elreldm  5807  tz6.12c  6697  onminex  7524  rntpos  7907  smores  7991  seqomlem2  8089  f1domg  8531  php  8703  fodomnum  9485  carduniima  9524  cardmin  9988  negn0  11071  sqrmo  14613  isch3  29020  cgrtriv  33465  wl-lem-moexsb  34806  grpomndo  35155  elghomlem2OLD  35166  tz6.12c-afv2  43448