Theorem sylanl1 676

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)

Hypotheses

Ref	Expression
sylanl1.1	⊢ (𝜑 → 𝜓)
sylanl1.2	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
sylanl1	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem sylanl1

Step	Hyp	Ref	Expression
1		sylanl1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	anim1i 614	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 579	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  adantlll  714  adantllr  715  adantl3r  746  isocnv  7181  f1iun  7760  odi  8372  oeoelem  8391  mapxpen  8879  xadddilem  12957  hashgt23el  14067  pcqmul  16482  infpnlem1  16539  setsn0fun  16802  chpdmat  21898  neitr  22239  hausflimi  23039  nmoix  23799  nmoleub  23801  metdsre  23922  bncssbn  24443  usgr2edg  27480  usgr2edg1  27482  crctcshwlkn0  28087  unoplin  30183  hmoplin  30205  chirredlem1  30653  mdsymlem2  30667  foresf1o  30751  zarcls1  31721  ordtconnlem1  31776  signstfvn  32448  isbasisrelowllem1  35453  isbasisrelowllem2  35454  pibt2  35515  lindsadd  35697  lindsdom  35698  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem25  35729  poimirlem29  35733  heicant  35739  cnambfre  35752  itg2addnclem  35755  ftc1anclem5  35781  ftc1anc  35785  rrnequiv  35920  isfldidl  36153  ispridlc  36155  supxrgelem  42766  supminfxr  42894  itcovalt2lem2  45910  reccot  46346  rectan  46347