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  258  bija  369  equvini  2492  equvel  2493  2eu6  2707  rgen2a  3126  rexraleqim  3478  elreldm  5486  tz6.12c  6352  onminex  7152  rntpos  7515  smores  7600  seqomlem2  7697  f1domg  8127  php  8298  fodomnum  9078  carduniima  9117  cardmin  9586  negn0  10659  sqrmo  14193  isch3  28431  cgrtriv  32439  wl-lem-moexsb  33677  grpomndo  33999  elghomlem2OLD  34010