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  1841  ax13lem1  2374  ax13lem2  2376  axc11n  2426  rspc6v  3593  reuss2  4273  reupick  4276  elinxp  5967  ordtr2  6351  suc11  6415  funimass4  6886  fliftfun  7246  omlimcl  8493  nneob  8571  rankwflemb  9686  cflm  10141  domtriomlem  10333  grothomex  10720  sup3  12079  caubnd  15266  fbflim2  23892  ellimc3  25807  usgruspgrb  29161  usgredgsscusgredg  29438  3cyclfrgrrn1  30265  dfon2lem6  35830  opnrebl2  36363  bj-nfimt  36680  axc11n11r  36725  bj-nnf-alrim  36797  stdpc5t  36869  wl-ax13lem1  37536  diaintclN  41105  dibintclN  41214  dihintcl  41391  sn-sup3d  42533  dflim5  43370  pm11.71  44438  axc11next  44447  rrx2plord2  48762