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  3345  rexraleqim  3613  elreldm  5899  tz6.12cOLD  6885  onminex  7778  rntpos  8218  smores  8321  seqomlem2  8419  f1domg  8943  php  9171  fodomnum  10010  carduniima  10049  cardmin  10517  negn0  11607  sqrmo  15217  isch3  31170  cgrtriv  35990  wl-lem-moexsb  37556  grpomndo  37869  elghomlem2OLD  37880  tz6.12c-afv2  47243