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  5395  fununi  6611  dfimafn  6941  funimass3  7044  isomin  7330  oneqmin  7794  tz7.48lem  8455  fisupg  9296  fiinfg  9513  trcl  9742  coflim  10275  coftr  10287  axdc3lem2  10465  konigthlem  10582  indpi  10921  nnsub  12284  2ndc1stc  23389  kgencn2  23495  tx1stc  23588  filuni  23823  fclscf  23963  alexsubALTlem2  23986  alexsubALTlem3  23987  alexsubALT  23989  nodenselem8  27655  n0subs  28305  lpni  30461  dfimafnf  32614  dfon2lem6  35806  bj-nnf-exlim  36774  finixpnum  37629  heiborlem4  37838  lncvrelatN  39800  imbi13  44545  relpmin  44977  dfaimafn  47194  sgoldbeven3prm  47797