Theorem syl9r 78

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 77	. 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:  peirceroll  85  imim12  105  sylan9r  508  19.38b  1843  ax12v2  2187  axprlem3  5371  fununi  6568  dfimafn  6897  funimass3  7001  isomin  7285  oneqmin  7747  tz7.48lem  8374  fisupg  9192  fiinfg  9408  trcl  9641  coflim  10175  coftr  10187  axdc3lem2  10365  konigthlem  10483  indpi  10822  nnsub  12193  2ndc1stc  23399  kgencn2  23505  tx1stc  23598  filuni  23833  fclscf  23973  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALT  23999  nodenselem8  27663  n0subs  28342  lpni  30538  dfimafnf  32696  r1omhfb  35249  r1omhfbregs  35274  dfon2lem6  35961  bj-nnf-exlim  36932  finixpnum  37777  heiborlem4  37986  lncvrelatN  40078  imbi13  44797  relpmin  45229  dfaimafn  47447  sgoldbeven3prm  48065