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  261  bija  373  equviniOLD  2393  equvel  2394  2eu6  2690  rgen2a  3171  rexraleqim  3550  elreldm  5646  tz6.12c  6522  onminex  7337  rntpos  7707  smores  7792  seqomlem2  7889  f1domg  8325  php  8496  fodomnum  9276  carduniima  9315  cardmin  9783  negn0  10869  sqrmo  14471  isch3  28813  cgrtriv  33017  wl-lem-moexsb  34278  grpomndo  34628  elghomlem2OLD  34639  tz6.12c-afv2  42877