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  2455  2eu6  2651  rgen2a  3347  rexraleqim  3616  elreldm  5902  tz6.12cOLD  6888  onminex  7781  rntpos  8221  smores  8324  seqomlem2  8422  f1domg  8946  php  9177  fodomnum  10017  carduniima  10056  cardmin  10524  negn0  11614  sqrmo  15224  isch3  31177  cgrtriv  35997  wl-lem-moexsb  37563  grpomndo  37876  elghomlem2OLD  37887  tz6.12c-afv2  47247