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  268  bija  381  equvel  2454  2eu6  2651  rgen2a  3342  rexraleqim  3600  elreldm  5895  tz6.12cOLD  6874  onminex  7742  rntpos  8175  smores  8303  seqomlem2  8402  f1domg  8919  php  9161  phpOLD  9173  fodomnum  10002  carduniima  10041  cardmin  10509  negn0  11593  sqrmo  15148  isch3  30246  cgrtriv  34663  wl-lem-moexsb  36096  grpomndo  36407  elghomlem2OLD  36418  tz6.12c-afv2  45594