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  2379  ax13lem2  2381  axc11n  2431  rspc6v  3643  reuss2  4326  reupick  4329  elinxp  6037  ordtr2  6428  suc11  6491  funimass4  6973  fliftfun  7332  omlimcl  8616  nneob  8694  rankwflemb  9833  cflm  10290  domtriomlem  10482  grothomex  10869  sup3  12225  caubnd  15397  fbflim2  23985  ellimc3  25914  usgruspgrb  29200  usgredgsscusgredg  29477  3cyclfrgrrn1  30304  dfon2lem6  35789  opnrebl2  36322  bj-nfimt  36639  axc11n11r  36684  bj-nnf-alrim  36756  stdpc5t  36828  wl-ax13lem1  37495  diaintclN  41060  dibintclN  41169  dihintcl  41346  sn-sup3d  42502  dflim5  43342  pm11.71  44416  axc11next  44425  rrx2plord2  48643