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  7264  f1iun  7876  odi  8494  oeoelem  8513  mapxpen  9056  xadddilem  13193  hashgt23el  14331  pcqmul  16765  infpnlem1  16822  setsn0fun  17084  chpdmat  22757  neitr  23096  hausflimi  23896  nmoix  24645  nmoleub  24647  metdsre  24770  bncssbn  25302  usgr2edg  29189  usgr2edg1  29191  crctcshwlkn0  29800  unoplin  31898  hmoplin  31920  chirredlem1  32368  mdsymlem2  32382  foresf1o  32482  zarcls1  33880  ordtconnlem1  33935  signstfvn  34580  isbasisrelowllem1  37395  isbasisrelowllem2  37396  pibt2  37457  lindsadd  37659  lindsdom  37660  matunitlindflem1  37662  matunitlindflem2  37663  poimirlem25  37691  poimirlem29  37695  heicant  37701  cnambfre  37714  itg2addnclem  37717  ftc1anclem5  37743  ftc1anc  37747  rrnequiv  37881  isfldidl  38114  ispridlc  38116  supxrgelem  45382  supminfxr  45508  uhgrimisgrgric  47968  cycl3grtri  47984  gpg5nbgrvtx03star  48117  gpg5nbgr3star  48118  itcovalt2lem2  48714  reccot  49796  rectan  49797