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  1840  ax13lem1  2373  ax13lem2  2375  axc11n  2425  rspc6v  3612  reuss2  4292  reupick  4295  elinxp  5993  ordtr2  6380  suc11  6444  funimass4  6928  fliftfun  7290  omlimcl  8545  nneob  8623  rankwflemb  9753  cflm  10210  domtriomlem  10402  grothomex  10789  sup3  12147  caubnd  15332  fbflim2  23871  ellimc3  25787  usgruspgrb  29117  usgredgsscusgredg  29394  3cyclfrgrrn1  30221  dfon2lem6  35783  opnrebl2  36316  bj-nfimt  36633  axc11n11r  36678  bj-nnf-alrim  36750  stdpc5t  36822  wl-ax13lem1  37489  diaintclN  41059  dibintclN  41168  dihintcl  41345  sn-sup3d  42487  dflim5  43325  pm11.71  44393  axc11next  44402  rrx2plord2  48715