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  2215  axprlem3  5387  fununi  6613  dfimafn  6945  funimass3  7051  isomin  7343  oneqmin  7812  tz7.48lemOLD  8444  fisupg  9272  fiinfg  9486  trcl  9722  coflim  10332  coftr  10344  axdc3lem2  10522  konigthlem  10646  indpi  10985  nnsub  12375  2ndc1stc  23762  kgencn2  23869  tx1stc  23962  filuni  24197  fclscf  24337  alexsubALTlem2  24360  alexsubALTlem3  24361  alexsubALT  24363  nodenselem8  28041  n0subs  28742  lpni  31075  dfimafnf  33223  r1omhfb  35727  r1omhfbregs  35788  dfon2lem6  36530  bj-nnf-exlim  37642  finixpnum  38508  heiborlem4  38728  lncvrelatN  40818  imbi13  45488  relpmin  45920  dfaimafn  48204  sgoldbeven3prm  48850