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  2454  2eu6  2650  rgen2a  3336  rexraleqim  3604  elreldm  5881  onminex  7742  rntpos  8179  smores  8282  seqomlem2  8380  f1domg  8904  php  9131  fodomnum  9970  carduniima  10009  cardmin  10477  negn0  11567  sqrmo  15176  isch3  31203  cgrtriv  35978  wl-lem-moexsb  37544  grpomndo  37857  elghomlem2OLD  37868  tz6.12c-afv2  47230