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  272  bija  385  equviniOLD  2467  equvel  2468  2eu6  2719  rgen2a  3193  rexraleqim  3588  elreldm  5769  tz6.12c  6670  onminex  7502  rntpos  7888  smores  7972  seqomlem2  8070  f1domg  8512  php  8685  fodomnum  9468  carduniima  9507  cardmin  9975  negn0  11058  sqrmo  14603  isch3  29024  cgrtriv  33576  wl-lem-moexsb  34969  grpomndo  35313  elghomlem2OLD  35324  tz6.12c-afv2  43798