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  1842  ax12v2  2182  axprlem3  5363  fununi  6556  dfimafn  6884  funimass3  6987  isomin  7271  oneqmin  7733  tz7.48lem  8360  fisupg  9172  fiinfg  9385  trcl  9618  coflim  10152  coftr  10164  axdc3lem2  10342  konigthlem  10459  indpi  10798  nnsub  12169  2ndc1stc  23367  kgencn2  23473  tx1stc  23566  filuni  23801  fclscf  23941  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALT  23967  nodenselem8  27631  n0subs  28290  lpni  30458  dfimafnf  32616  r1omhfb  35121  r1omhfbregs  35131  dfon2lem6  35828  bj-nnf-exlim  36796  finixpnum  37651  heiborlem4  37860  lncvrelatN  39826  imbi13  44559  relpmin  44991  dfaimafn  47202  sgoldbeven3prm  47820