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  2461  2eu6  2658  rgen2a  3334  rexraleqim  3590  elreldm  5884  onminex  7749  rntpos  8182  smores  8285  seqomlem2  8383  f1domg  8911  php  9134  fodomnum  9970  carduniima  10009  cardmin  10477  negn0  11570  sqrmo  15204  isch3  31327  cgrtriv  36200  axtco2  36672  dfttc4lem2  36727  wl-lem-moexsb  37907  grpomndo  38210  elghomlem2OLD  38221  tz6.12c-afv2  47702