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  2464  2eu6  2660  rgen2a  3379  rexraleqim  3660  elreldm  5960  tz6.12cOLD  6947  onminex  7838  rntpos  8280  smores  8408  seqomlem2  8507  f1domg  9032  php  9273  phpOLD  9285  fodomnum  10126  carduniima  10165  cardmin  10633  negn0  11719  sqrmo  15300  isch3  31273  cgrtriv  35966  wl-lem-moexsb  37522  grpomndo  37835  elghomlem2OLD  37846  tz6.12c-afv2  47157