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:  sylan9r  505  19.38b  1937  ax12v2  2215  fununi  6175  dfimafn  6470  funimass3  6559  isomin  6815  oneqmin  7239  tz7.48lem  7775  fisupg  8450  fiinfg  8647  trcl  8854  coflim  9371  coftr  9383  axdc3lem2  9561  konigthlem  9678  indpi  10017  nnsub  11357  2ndc1stc  21583  kgencn2  21689  tx1stc  21782  filuni  22017  fclscf  22157  alexsubALTlem2  22180  alexsubALTlem3  22181  alexsubALT  22183  lpni  27860  dfimafnf  29955  dfon2lem6  32205  nodenselem8  32354  bj-exlalrim  33109  finixpnum  33883  heiborlem4  34100  lncvrelatN  35802  imbi13  39506  dfaimafn  42019  sgoldbeven3prm  42453