Theorem syli 40

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 33	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	sylcom 31	1 ⊢ (𝜓 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  ibd  272  bija  383  equvel  2485  2eu6  2681  rgen2a  3356  rexraleqim  3600  elreldm  5916  onminex  7817  rntpos  8260  smores  8364  seqomlem2  8465  f1domg  9002  php  9226  fodomnum  10140  carduniima  10179  cardmin  10652  negn0  11749  sqrmo  15424  isch3  31849  acwer1prclem  35816  onprcf1acwevdlem1  35965  cgrtriv  36860  axtco2  37355  dfttc4lem2  37410  wl-lem-moexsb  38594  grpomndo  38903  elghomlem2OLD  38914  tz6.12c-afv2  48406