Theorem sylanl1 677

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 615	. 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 206  df-an 397

This theorem is referenced by:  adantlll  715  adantllr  716  adantl3r  747  isocnv  7201  f1iun  7786  odi  8410  oeoelem  8429  mapxpen  8930  xadddilem  13028  hashgt23el  14139  pcqmul  16554  infpnlem1  16611  setsn0fun  16874  chpdmat  21990  neitr  22331  hausflimi  23131  nmoix  23893  nmoleub  23895  metdsre  24016  bncssbn  24538  usgr2edg  27577  usgr2edg1  27579  crctcshwlkn0  28186  unoplin  30282  hmoplin  30304  chirredlem1  30752  mdsymlem2  30766  foresf1o  30850  zarcls1  31819  ordtconnlem1  31874  signstfvn  32548  isbasisrelowllem1  35526  isbasisrelowllem2  35527  pibt2  35588  lindsadd  35770  lindsdom  35771  matunitlindflem1  35773  matunitlindflem2  35774  poimirlem25  35802  poimirlem29  35806  heicant  35812  cnambfre  35825  itg2addnclem  35828  ftc1anclem5  35854  ftc1anc  35858  rrnequiv  35993  isfldidl  36226  ispridlc  36228  supxrgelem  42876  supminfxr  43004  itcovalt2lem2  46022  reccot  46460  rectan  46461