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  508  19.38a  1842  ax13lem1  2374  ax13lem2  2376  axc11n  2426  reuss2  4249  reupick  4252  elinxp  5929  ordtr2  6310  suc11  6369  funimass4  6834  fliftfun  7183  omlimcl  8409  nneob  8486  rankwflemb  9551  cflm  10006  domtriomlem  10198  grothomex  10585  sup3  11932  caubnd  15070  fbflim2  23128  ellimc3  25043  usgruspgrb  27551  usgredgsscusgredg  27826  3cyclfrgrrn1  28649  dfon2lem6  33764  opnrebl2  34510  bj-nfimt  34819  axc11n11r  34865  bj-nnf-alrim  34937  stdpc5t  35010  wl-ax13lem1  35665  diaintclN  39072  dibintclN  39181  dihintcl  39358  pm11.71  42015  axc11next  42024  rrx2plord2  46068