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  382  equvel  2454  2eu6  2656  rgen2a  3297  rexraleqim  3582  elreldm  5856  tz6.12cOLD  6831  onminex  7684  rntpos  8086  smores  8214  seqomlem2  8313  f1domg  8793  php  9031  phpOLD  9043  fodomnum  9859  carduniima  9898  cardmin  10366  negn0  11450  sqrmo  15008  isch3  29648  cgrtriv  34349  wl-lem-moexsb  35767  grpomndo  36077  elghomlem2OLD  36088  tz6.12c-afv2  44792