Theorem syl9 77

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Hypotheses

Ref	Expression
syl9.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl9.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
syl9	⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Proof of Theorem syl9

Step	Hyp	Ref	Expression
1		syl9.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏)))
4	1, 3	syl5d 73	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:  syl9r  78  com23  86  sylan9  507  19.38a  1843  ax13lem1  2374  ax13lem2  2376  axc11n  2426  reuss2  4246  reupick  4249  elinxp  5918  ordtr2  6295  suc11  6354  funimass4  6816  fliftfun  7163  omlimcl  8371  nneob  8446  rankwflemb  9482  cflm  9937  domtriomlem  10129  grothomex  10516  sup3  11862  caubnd  14998  fbflim2  23036  ellimc3  24948  usgruspgrb  27454  usgredgsscusgredg  27729  3cyclfrgrrn1  28550  dfon2lem6  33670  opnrebl2  34437  bj-nfimt  34746  axc11n11r  34792  bj-nnf-alrim  34864  stdpc5t  34937  wl-ax13lem1  35592  diaintclN  38999  dibintclN  39108  dihintcl  39285  pm11.71  41904  axc11next  41913  rrx2plord2  45956