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 ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  peirceroll  86  imim12  106  expt  178  sylan9r  518  19.38b  1874  ax12v2  2218  axprlem3  5394  fununi  6645  dfimafn  6978  funimass3  7084  isomin  7376  oneqmin  7848  tz7.48lemOLD  8489  fisupg  9317  fiinfg  9530  trcl  9766  coflim  10378  coftr  10390  axdc3lem2  10568  konigthlem  10692  indpi  11031  nnsub  12422  2ndc1stc  23824  kgencn2  23931  tx1stc  24024  filuni  24259  fclscf  24399  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALT  24425  nodenselem8  28105  n0subs  28806  lpni  31139  dfimafnf  33328  eqhf  35861  eqhfregs  35946  dfon2lem6  36765  bj-nnf-exlim  37877  finixpnum  38796  heiborlem4  39014  lncvrelatN  41104  imbi13  45763  relpmin  46206  dfaimafn  48508  sgoldbeven3prm  49154