Theorem sylanl1 680

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 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 207  df-an 396

This theorem is referenced by:  adantlll  718  adantllr  719  adantl3r  750  isocnv  7308  f1iun  7925  odi  8546  oeoelem  8565  mapxpen  9113  xadddilem  13261  hashgt23el  14396  pcqmul  16831  infpnlem1  16888  setsn0fun  17150  chpdmat  22735  neitr  23074  hausflimi  23874  nmoix  24624  nmoleub  24626  metdsre  24749  bncssbn  25281  usgr2edg  29144  usgr2edg1  29146  crctcshwlkn0  29758  unoplin  31856  hmoplin  31878  chirredlem1  32326  mdsymlem2  32340  foresf1o  32440  zarcls1  33866  ordtconnlem1  33921  signstfvn  34567  isbasisrelowllem1  37350  isbasisrelowllem2  37351  pibt2  37412  lindsadd  37614  lindsdom  37615  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem25  37646  poimirlem29  37650  heicant  37656  cnambfre  37669  itg2addnclem  37672  ftc1anclem5  37698  ftc1anc  37702  rrnequiv  37836  isfldidl  38069  ispridlc  38071  supxrgelem  45340  supminfxr  45467  uhgrimisgrgric  47935  cycl3grtri  47950  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  itcovalt2lem2  48669  reccot  49751  rectan  49752