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  2456  2eu6  2652  rgen2a  3337  rexraleqim  3597  elreldm  5870  onminex  7730  rntpos  8164  smores  8267  seqomlem2  8365  f1domg  8889  php  9111  fodomnum  9943  carduniima  9982  cardmin  10450  negn0  11541  sqrmo  15153  isch3  31213  cgrtriv  36036  wl-lem-moexsb  37602  grpomndo  37915  elghomlem2OLD  37926  tz6.12c-afv2  47273