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  1841  ax12v2  2180  axprlem3  5380  fununi  6591  dfimafn  6923  funimass3  7026  isomin  7312  oneqmin  7776  tz7.48lem  8409  fisupg  9235  fiinfg  9452  trcl  9681  coflim  10214  coftr  10226  axdc3lem2  10404  konigthlem  10521  indpi  10860  nnsub  12230  2ndc1stc  23338  kgencn2  23444  tx1stc  23537  filuni  23772  fclscf  23912  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALT  23938  nodenselem8  27603  n0subs  28253  lpni  30409  dfimafnf  32560  dfon2lem6  35776  bj-nnf-exlim  36744  finixpnum  37599  heiborlem4  37808  lncvrelatN  39775  imbi13  44510  relpmin  44942  dfaimafn  47166  sgoldbeven3prm  47784