Theorem syli 40

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 33	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	sylcom 31	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  272  bija  383  equvel  2488  2eu6  2684  rgen2a  3360  rexraleqim  3607  elreldm  5927  onminex  7802  rntpos  8236  smores  8340  seqomlem2  8439  f1domg  8969  php  9192  fodomnum  10042  carduniima  10081  cardmin  10549  negn0  11644  sqrmo  15304  isch3  31574  cgrtriv  36475  axtco2  36966  dfttc4lem2  37021  wl-lem-moexsb  38204  grpomndo  38507  elghomlem2OLD  38518  tz6.12c-afv2  47962