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  381  equvel  2457  2eu6  2659  rgen2a  3157  rexraleqim  3577  elreldm  5841  tz6.12c  6793  onminex  7642  rntpos  8039  smores  8167  seqomlem2  8266  f1domg  8731  php  8957  phpOLD  8970  fodomnum  9797  carduniima  9836  cardmin  10304  negn0  11387  sqrmo  14944  isch3  29582  cgrtriv  34283  wl-lem-moexsb  35702  grpomndo  36012  elghomlem2OLD  36023  tz6.12c-afv2  44685