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  268  bija  379  equvel  2449  2eu6  2645  rgen2a  3354  rexraleqim  3630  elreldm  5937  tz6.12cOLD  6923  onminex  7806  rntpos  8245  smores  8373  seqomlem2  8472  f1domg  8993  php  9238  phpOLD  9250  fodomnum  10087  carduniima  10126  cardmin  10594  negn0  11680  sqrmo  15242  isch3  31143  cgrtriv  35749  wl-lem-moexsb  37186  grpomndo  37499  elghomlem2OLD  37510  tz6.12c-afv2  46765