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  2459  2eu6  2655  rgen2a  3369  rexraleqim  3647  elreldm  5949  tz6.12cOLD  6934  onminex  7822  rntpos  8263  smores  8391  seqomlem2  8490  f1domg  9011  php  9245  phpOLD  9257  fodomnum  10095  carduniima  10134  cardmin  10602  negn0  11690  sqrmo  15287  isch3  31270  cgrtriv  35984  wl-lem-moexsb  37549  grpomndo  37862  elghomlem2OLD  37873  tz6.12c-afv2  47192