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  2408  ax13lem2  2410  axc11n  2460  rspc6v  3604  reuss2  4279  reupick  4282  axprglem  5409  elinxp  6020  ordtr2  6410  suc11  6474  funimass4  6949  fliftfun  7319  omlimcl  8569  nneob  8648  rankwflemb  9772  cflm  10248  domtriomlem  10441  grothomex  10829  sup3  12187  caubnd  15434  fbflim2  24185  ellimc3  26089  usgruspgrb  29591  usgredgsscusgredg  29867  3cyclfrgrrn1  30707  dfon2lem6  36315  opnrebl2  36889  axtco1from2  37043  bj-nfimt  37302  axc11n11r  37365  bj-nnf-alrim  37427  stdpc5t  37519  wl-ax13lem1  38197  diaintclN  41890  dibintclN  41999  dihintcl  42176  sn-sup3d  43324  dflim5  44114  pm11.71  45165  axc11next  45174  rrx2plord2  49559