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  510  19.38b  1841  ax12v2  2171  fununi  6538  dfimafn  6864  funimass3  6963  isomin  7240  oneqmin  7682  tz7.48lem  8303  fisupg  9106  fiinfg  9302  trcl  9530  coflim  10063  coftr  10075  axdc3lem2  10253  konigthlem  10370  indpi  10709  nnsub  12063  2ndc1stc  22647  kgencn2  22753  tx1stc  22846  filuni  23081  fclscf  23221  alexsubALTlem2  23244  alexsubALTlem3  23245  alexsubALT  23247  lpni  28887  dfimafnf  31016  dfon2lem6  33809  nodenselem8  33939  bj-nnf-exlim  34983  finixpnum  35806  heiborlem4  36016  lncvrelatN  37837  imbi13  42178  dfaimafn  44715  sgoldbeven3prm  45293