Theorem sylanl1 690

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 624	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 589	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  adantlll  728  adantllr  729  adantl3r  760  isocnv  7310  f1iun  7921  odi  8543  oeoelem  8563  mapxpen  9111  xadddilem  13294  hashgt23el  14434  pcqmul  16872  infpnlem1  16929  setsn0fun  17192  chpdmat  22881  neitr  23220  hausflimi  24020  nmoix  24769  nmoleub  24771  metdsre  24894  bncssbn  25416  usgr2edg  29357  usgr2edg1  29359  crctcshwlkn0  29967  unoplin  32069  hmoplin  32091  chirredlem1  32539  mdsymlem2  32553  foresf1o  32652  zarcls1  34127  ordtconnlem1  34182  signstfvn  34827  isbasisrelowllem1  37813  isbasisrelowllem2  37814  pibt2  37875  lindsadd  38076  lindsdom  38077  matunitlindflem1  38079  matunitlindflem2  38080  poimirlem25  38108  poimirlem29  38112  heicant  38118  cnambfre  38131  itg2addnclem  38134  ftc1anclem5  38160  ftc1anc  38164  rrnequiv  38298  isfldidl  38531  ispridlc  38533  supxrgelem  45877  supminfxr  46002  uhgrimisgrgric  48517  cycl3grtri  48533  gpg5nbgrvtx03star  48666  gpg5nbgr3star  48667  itcovalt2lem2  49262  reccot  50343  rectan  50344