Theorem syl9r 75

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)

Hypotheses

Ref	Expression
syl9r.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl9r.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
syl9r	⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏)))

Proof of Theorem syl9r

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl9r.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9 74	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	com12 32	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:  sylan9r  687  ax12v2  2033  ax12vOLD  2034  ax12vOLDOLD  2035  nfimdOLD  2208  fununi  5860  dfimafn  6136  funimass3  6222  isomin  6461  oneqmin  6870  tz7.48lem  7396  fisupg  8066  fiinfg  8261  trcl  8460  coflim  8939  coftr  8951  axdc3lem2  9129  konigthlem  9242  indpi  9581  nnsub  10902  2ndc1stc  21002  kgencn2  21108  tx1stc  21201  filuni  21437  fclscf  21577  alexsubALTlem2  21600  alexsubALTlem3  21601  alexsubALT  21603  lpni  26484  dfimafnf  28619  dfon2lem6  30739  nodenselem8  30889  finixpnum  32363  heiborlem4  32582  lncvrelatN  33884  imbi13  37546  dfaimafn  39695