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  expt  177  sylan9r  513  19.38b  1848  ax12v2  2191  axprlem3  5354  fununi  6560  dfimafn  6889  funimass3  6995  isomin  7281  oneqmin  7743  tz7.48lem  8370  fisupg  9188  fiinfg  9404  trcl  9640  coflim  10174  coftr  10186  axdc3lem2  10364  konigthlem  10482  indpi  10821  nnsub  12212  2ndc1stc  23434  kgencn2  23540  tx1stc  23633  filuni  23868  fclscf  24008  alexsubALTlem2  24031  alexsubALTlem3  24032  alexsubALT  24034  nodenselem8  27673  n0subs  28373  lpni  30569  dfimafnf  32728  r1omhfb  35293  r1omhfbregs  35318  dfon2lem6  36014  bj-nnf-exlim  37103  finixpnum  37972  heiborlem4  38181  lncvrelatN  40273  imbi13  44964  relpmin  45396  dfaimafn  47628  sgoldbeven3prm  48274