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  508  19.38a  1842  ax13lem1  2373  ax13lem2  2375  axc11n  2425  rspc6v  3631  reuss2  4315  reupick  4318  elinxp  6019  ordtr2  6408  suc11  6471  funimass4  6956  fliftfun  7311  omlimcl  8580  nneob  8657  rankwflemb  9790  cflm  10247  domtriomlem  10439  grothomex  10826  sup3  12173  caubnd  15307  fbflim2  23488  ellimc3  25403  usgruspgrb  28479  usgredgsscusgredg  28754  3cyclfrgrrn1  29576  dfon2lem6  34835  opnrebl2  35298  bj-nfimt  35607  axc11n11r  35653  bj-nnf-alrim  35725  stdpc5t  35797  wl-ax13lem1  36467  diaintclN  40021  dibintclN  40130  dihintcl  40307  dflim5  42167  pm11.71  43244  axc11next  43253  rrx2plord2  47492