Theorem syl9 78

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 74	1 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl9r  79  com23  87  sylan9  517  19.38a  1873  ax13lem1  2403  ax13lem2  2405  axc11n  2455  rspc6v  3597  reuss2  4272  reupick  4275  axprglem  5401  elinxp  6012  ordtr2  6403  suc11  6467  funimass4  6942  fliftfun  7313  omlimcl  8565  nneob  8644  rankwflemb  9775  cflm  10251  domtriomlem  10444  grothomex  10838  sup3  12196  caubnd  15446  fbflim2  24203  ellimc3  26106  usgruspgrb  29643  usgredgsscusgredg  29919  3cyclfrgrrn1  30765  dfon2lem6  36365  opnrebl2  36940  axtco1from2  37094  bj-nfimt  37353  axc11n11r  37416  bj-nnf-alrim  37478  stdpc5t  37570  wl-ax13lem1  38248  diaintclN  41931  dibintclN  42040  dihintcl  42217  sn-sup3d  43380  dflim5  44170  pm11.71  45221  axc11next  45230  rrx2plord2  49652