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  5372  fununi  6575  dfimafn  6904  funimass3  7008  isomin  7293  oneqmin  7755  tz7.48lem  8382  fisupg  9200  fiinfg  9416  trcl  9649  coflim  10183  coftr  10195  axdc3lem2  10373  konigthlem  10491  indpi  10830  nnsub  12201  2ndc1stc  23407  kgencn2  23513  tx1stc  23606  filuni  23841  fclscf  23981  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALT  24007  nodenselem8  27671  n0subs  28371  lpni  30567  dfimafnf  32725  r1omhfb  35287  r1omhfbregs  35312  dfon2lem6  35999  bj-nnf-exlim  37000  finixpnum  37853  heiborlem4  38062  lncvrelatN  40154  imbi13  44873  relpmin  45305  dfaimafn  47522  sgoldbeven3prm  48140