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  2461  2eu6  2658  rgen2a  3343  rexraleqim  3603  elreldm  5892  onminex  7757  rntpos  8191  smores  8294  seqomlem2  8392  f1domg  8920  php  9143  fodomnum  9979  carduniima  10018  cardmin  10486  negn0  11578  sqrmo  15186  isch3  31328  cgrtriv  36215  wl-lem-moexsb  37820  grpomndo  38123  elghomlem2OLD  38134  tz6.12c-afv2  47599