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  1841  ax12v2  2179  axprlem3  5425  fununi  6641  dfimafn  6971  funimass3  7074  isomin  7357  oneqmin  7820  tz7.48lem  8481  fisupg  9324  fiinfg  9539  trcl  9768  coflim  10301  coftr  10313  axdc3lem2  10491  konigthlem  10608  indpi  10947  nnsub  12310  2ndc1stc  23459  kgencn2  23565  tx1stc  23658  filuni  23893  fclscf  24033  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALT  24059  nodenselem8  27736  n0subs  28360  lpni  30499  dfimafnf  32646  dfon2lem6  35789  bj-nnf-exlim  36757  finixpnum  37612  heiborlem4  37821  lncvrelatN  39783  imbi13  44540  relpmin  44973  dfaimafn  47177  sgoldbeven3prm  47770