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  693  ax12v2  2198  nfimdOLD  2371  fununi  6125  dfimafn  6408  funimass3  6497  isomin  6751  oneqmin  7171  tz7.48lem  7706  fisupg  8375  fiinfg  8572  trcl  8779  coflim  9295  coftr  9307  axdc3lem2  9485  konigthlem  9602  indpi  9941  nnsub  11271  2ndc1stc  21476  kgencn2  21582  tx1stc  21675  filuni  21910  fclscf  22050  alexsubALTlem2  22073  alexsubALTlem3  22074  alexsubALT  22076  lpni  27664  dfimafnf  29766  dfon2lem6  32019  nodenselem8  32168  finixpnum  33725  heiborlem4  33944  lncvrelatN  35588  imbi13  39246  dfaimafn  41769  sgoldbeven3prm  42199