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  1842  ax13lem1  2378  ax13lem2  2380  axc11n  2430  rspc6v  3585  reuss2  4266  reupick  4269  axprglem  5378  elinxp  5984  ordtr2  6368  suc11  6432  funimass4  6904  fliftfun  7267  omlimcl  8513  nneob  8592  rankwflemb  9717  cflm  10172  domtriomlem  10364  grothomex  10752  sup3  12113  caubnd  15321  fbflim2  23942  ellimc3  25846  usgruspgrb  29252  usgredgsscusgredg  29528  3cyclfrgrrn1  30355  dfon2lem6  35968  opnrebl2  36503  axtco1from2  36657  bj-nfimt  36917  axc11n11r  36980  bj-nnf-alrim  37042  stdpc5t  37134  wl-ax13lem1  37810  diaintclN  41504  dibintclN  41613  dihintcl  41790  sn-sup3d  42937  dflim5  43757  pm11.71  44824  axc11next  44833  rrx2plord2  49198