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  382  equvel  2456  2eu6  2653  rgen2a  3368  rexraleqim  3636  elreldm  5935  tz6.12cOLD  6919  onminex  7790  rntpos  8224  smores  8352  seqomlem2  8451  f1domg  8968  php  9210  phpOLD  9222  fodomnum  10052  carduniima  10091  cardmin  10559  negn0  11643  sqrmo  15198  isch3  30494  cgrtriv  34974  wl-lem-moexsb  36433  grpomndo  36743  elghomlem2OLD  36754  tz6.12c-afv2  45950