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  2656  rgen2a  3350  rexraleqim  3626  elreldm  5915  tz6.12cOLD  6903  onminex  7796  rntpos  8238  smores  8366  seqomlem2  8465  f1domg  8986  php  9221  phpOLD  9231  fodomnum  10071  carduniima  10110  cardmin  10578  negn0  11666  sqrmo  15270  isch3  31222  cgrtriv  36020  wl-lem-moexsb  37586  grpomndo  37899  elghomlem2OLD  37910  tz6.12c-afv2  47271