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  5398  fununi  6615  dfimafn  6947  funimass3  7053  isomin  7341  oneqmin  7801  tz7.48lem  8430  fisupg  9251  fiinfg  9464  trcl  9700  coflim  10256  coftr  10268  axdc3lem2  10446  konigthlem  10564  indpi  10903  nnsub  12291  2ndc1stc  23637  kgencn2  23743  tx1stc  23836  filuni  24071  fclscf  24211  alexsubALTlem2  24234  alexsubALTlem3  24235  alexsubALT  24237  nodenselem8  27884  n0subs  28585  lpni  30861  dfimafnf  33010  r1omhfb  35525  r1omhfbregs  35566  dfon2lem6  36291  bj-nnf-exlim  37418  finixpnum  38289  heiborlem4  38498  lncvrelatN  40588  imbi13  45262  relpmin  45694  dfaimafn  47935  sgoldbeven3prm  48581