Theorem sylanl1 679

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 579	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  717  adantllr  718  adantl3r  749  isocnv  7366  f1iun  7984  odi  8635  oeoelem  8654  mapxpen  9209  xadddilem  13356  hashgt23el  14473  pcqmul  16900  infpnlem1  16957  setsn0fun  17220  chpdmat  22868  neitr  23209  hausflimi  24009  nmoix  24771  nmoleub  24773  metdsre  24894  bncssbn  25427  usgr2edg  29245  usgr2edg1  29247  crctcshwlkn0  29854  unoplin  31952  hmoplin  31974  chirredlem1  32422  mdsymlem2  32436  foresf1o  32532  zarcls1  33815  ordtconnlem1  33870  signstfvn  34546  isbasisrelowllem1  37321  isbasisrelowllem2  37322  pibt2  37383  lindsadd  37573  lindsdom  37574  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem25  37605  poimirlem29  37609  heicant  37615  cnambfre  37628  itg2addnclem  37631  ftc1anclem5  37657  ftc1anc  37661  rrnequiv  37795  isfldidl  38028  ispridlc  38030  supxrgelem  45252  supminfxr  45379  uhgrimisgrgric  47783  itcovalt2lem2  48410  reccot  48850  rectan  48851