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  512  19.38b  1842  ax12v2  2177  fununi  6415  dfimafn  6721  funimass3  6820  isomin  7090  oneqmin  7525  tz7.48lem  8093  fisupg  8812  fiinfg  9009  trcl  9216  coflim  9734  coftr  9746  axdc3lem2  9924  konigthlem  10041  indpi  10380  nnsub  11731  2ndc1stc  22165  kgencn2  22271  tx1stc  22364  filuni  22599  fclscf  22739  alexsubALTlem2  22762  alexsubALTlem3  22763  alexsubALT  22765  lpni  28376  dfimafnf  30507  dfon2lem6  33293  nodenselem8  33492  bj-nnf-exlim  34516  finixpnum  35357  heiborlem4  35567  lncvrelatN  37392  imbi13  41644  dfaimafn  44148  sgoldbeven3prm  44727