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  2460  2eu6  2657  rgen2a  3333  rexraleqim  3589  elreldm  5890  onminex  7756  rntpos  8189  smores  8292  seqomlem2  8390  f1domg  8918  php  9141  fodomnum  9979  carduniima  10018  cardmin  10486  negn0  11579  sqrmo  15213  isch3  31312  cgrtriv  36184  axtco2  36656  dfttc4lem2  36711  wl-lem-moexsb  37893  grpomndo  38196  elghomlem2OLD  38207  tz6.12c-afv2  47690