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  260  bija  371  equvini  2504  equvel  2505  2eu6  2720  rgen2a  3163  rexraleqim  3520  elreldm  5549  tz6.12c  6431  onminex  7235  rntpos  7598  smores  7683  seqomlem2  7780  f1domg  8210  php  8381  fodomnum  9161  carduniima  9200  cardmin  9669  negn0  10742  sqrmo  14213  isch3  28424  cgrtriv  32428  wl-lem-moexsb  33662  grpomndo  33983  elghomlem2OLD  33994  tz6.12c-afv2  41829