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  5879  onminex  7741  rntpos  8175  smores  8278  seqomlem2  8376  f1domg  8900  php  9123  fodomnum  9955  carduniima  9994  cardmin  10462  negn0  11553  sqrmo  15160  isch3  31223  cgrtriv  36067  wl-lem-moexsb  37633  grpomndo  37935  elghomlem2OLD  37946  tz6.12c-afv2  47366