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  1873  ax12v2  2214  axprlem3  5386  fununi  6616  dfimafn  6948  funimass3  7054  isomin  7346  oneqmin  7815  tz7.48lemOLD  8455  fisupg  9283  fiinfg  9497  trcl  9733  coflim  10343  coftr  10355  axdc3lem2  10533  konigthlem  10657  indpi  10996  nnsub  12386  2ndc1stc  23775  kgencn2  23882  tx1stc  23975  filuni  24210  fclscf  24350  alexsubALTlem2  24373  alexsubALTlem3  24374  alexsubALT  24376  nodenselem8  28054  n0subs  28755  lpni  31088  dfimafnf  33278  r1omhfb  35791  r1omhfbregs  35862  dfon2lem6  36643  bj-nnf-exlim  37755  finixpnum  38622  heiborlem4  38842  lncvrelatN  40932  imbi13  45597  relpmin  46036  dfaimafn  48329  sgoldbeven3prm  48975