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  2494  2eu6  2690  rgen2a  3367  rexraleqim  3615  elreldm  5923  onminex  7797  rntpos  8231  smores  8335  seqomlem2  8434  f1domg  8964  php  9187  fodomnum  10037  carduniima  10076  cardmin  10544  negn0  11639  sqrmo  15298  isch3  31530  cgrtriv  36389  axtco2  36870  dfttc4lem2  36925  wl-lem-moexsb  38106  grpomndo  38409  elghomlem2OLD  38420  tz6.12c-afv2  47861