Theorem syl9r 79

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 78	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	com12 33	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  86  imim12  106  expt  178  sylan9r  517  19.38b  1868  ax12v2  2221  axprlem3  5394  fununi  6608  dfimafn  6941  funimass3  7047  isomin  7333  oneqmin  7795  tz7.48lem  8424  fisupg  9244  fiinfg  9457  trcl  9693  coflim  10241  coftr  10253  axdc3lem2  10431  konigthlem  10549  indpi  10888  nnsub  12276  2ndc1stc  23573  kgencn2  23679  tx1stc  23772  filuni  24007  fclscf  24147  alexsubALTlem2  24170  alexsubALTlem3  24171  alexsubALT  24173  nodenselem8  27817  n0subs  28518  lpni  30769  dfimafnf  32918  r1omhfb  35444  r1omhfbregs  35469  dfon2lem6  36173  bj-nnf-exlim  37270  finixpnum  38139  heiborlem4  38348  lncvrelatN  40440  imbi13  45114  relpmin  45546  dfaimafn  47784  sgoldbeven3prm  48430