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 580	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  adantlll  714  adantllr  715  adantl3r  746  isocnv  6946  f1iun  7501  odi  8055  oeoelem  8074  mapxpen  8530  xadddilem  12537  hashgt23el  13633  pcqmul  16019  infpnlem1  16075  setsn0fun  16349  chpdmat  21133  neitr  21472  hausflimi  22272  nmoix  23021  nmoleub  23023  metdsre  23144  bncssbn  23660  usgr2edg  26675  usgr2edg1  26677  crctcshwlkn0  27286  unoplin  29388  hmoplin  29410  chirredlem1  29858  mdsymlem2  29872  foresf1o  29957  ordtconnlem1  30784  isbasisrelowllem1  34186  isbasisrelowllem2  34187  pibt2  34248  lindsadd  34435  lindsdom  34436  matunitlindflem1  34438  matunitlindflem2  34439  poimirlem25  34467  poimirlem29  34471  heicant  34477  cnambfre  34490  itg2addnclem  34493  ftc1anclem5  34521  ftc1anc  34525  rrnequiv  34664  isfldidl  34897  ispridlc  34899  supxrgelem  41165  supminfxr  41301  reccot  44357  rectan  44358