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  270  bija  381  equvel  2464  2eu6  2660  rgen2a  3335  rexraleqim  3585  elreldm  5877  onminex  7745  rntpos  8179  smores  8282  seqomlem2  8380  f1domg  8908  php  9131  fodomnum  9970  carduniima  10009  cardmin  10477  negn0  11570  sqrmo  15204  isch3  31330  cgrtriv  36230  axtco2  36702  dfttc4lem2  36757  wl-lem-moexsb  37939  grpomndo  38242  elghomlem2OLD  38253  tz6.12c-afv2  47705