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  2458  2eu6  2654  rgen2a  3338  rexraleqim  3598  elreldm  5881  onminex  7744  rntpos  8178  smores  8281  seqomlem2  8379  f1domg  8904  php  9127  fodomnum  9959  carduniima  9998  cardmin  10466  negn0  11557  sqrmo  15165  isch3  31242  cgrtriv  36118  wl-lem-moexsb  37685  grpomndo  37988  elghomlem2OLD  37999  tz6.12c-afv2  47404