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  271  bija  382  equvel  2486  2eu6  2682  rgen2a  3357  rexraleqim  3605  elreldm  5907  onminex  7780  rntpos  8213  smores  8317  seqomlem2  8416  f1domg  8946  php  9169  fodomnum  10007  carduniima  10046  cardmin  10515  negn0  11610  sqrmo  15269  isch3  31401  cgrtriv  36313  axtco2  36795  dfttc4lem2  36850  wl-lem-moexsb  38032  grpomndo  38335  elghomlem2OLD  38346  tz6.12c-afv2  47797