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  1843  ax12v2  2187  axprlem3  5367  fununi  6573  dfimafn  6902  funimass3  7006  isomin  7292  oneqmin  7754  tz7.48lem  8380  fisupg  9198  fiinfg  9414  trcl  9649  coflim  10183  coftr  10195  axdc3lem2  10373  konigthlem  10491  indpi  10830  nnsub  12221  2ndc1stc  23416  kgencn2  23522  tx1stc  23615  filuni  23850  fclscf  23990  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALT  24016  nodenselem8  27655  n0subs  28355  lpni  30551  dfimafnf  32709  r1omhfb  35256  r1omhfbregs  35281  dfon2lem6  35968  bj-nnf-exlim  37057  finixpnum  37926  heiborlem4  38135  lncvrelatN  40227  imbi13  44947  relpmin  45379  dfaimafn  47613  sgoldbeven3prm  48259