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  382  equvel  2458  2eu6  2660  rgen2a  3158  rexraleqim  3578  elreldm  5843  tz6.12c  6796  onminex  7646  rntpos  8046  smores  8174  seqomlem2  8273  f1domg  8743  php  8974  phpOLD  8987  fodomnum  9814  carduniima  9853  cardmin  10321  negn0  11404  sqrmo  14961  isch3  29599  cgrtriv  34300  wl-lem-moexsb  35719  grpomndo  36029  elghomlem2OLD  36040  tz6.12c-afv2  44702