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  509  19.38b  1843  ax12v2  2173  fununi  6581  dfimafn  6910  funimass3  7009  isomin  7287  oneqmin  7740  tz7.48lem  8392  fisupg  9242  fiinfg  9444  trcl  9673  coflim  10206  coftr  10218  axdc3lem2  10396  konigthlem  10513  indpi  10852  nnsub  12206  2ndc1stc  22839  kgencn2  22945  tx1stc  23038  filuni  23273  fclscf  23413  alexsubALTlem2  23436  alexsubALTlem3  23437  alexsubALT  23439  nodenselem8  27076  lpni  29485  dfimafnf  31617  dfon2lem6  34449  bj-nnf-exlim  35297  finixpnum  36136  heiborlem4  36346  lncvrelatN  38317  imbi13  42924  dfaimafn  45517  sgoldbeven3prm  46095