Theorem sylanl1 681

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 616	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 581	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  719  adantllr  720  adantl3r  751  isocnv  7278  f1iun  7890  odi  8507  oeoelem  8527  mapxpen  9074  xadddilem  13237  hashgt23el  14377  pcqmul  16815  infpnlem1  16872  setsn0fun  17134  chpdmat  22816  neitr  23155  hausflimi  23955  nmoix  24704  nmoleub  24706  metdsre  24829  bncssbn  25351  usgr2edg  29293  usgr2edg1  29295  crctcshwlkn0  29904  unoplin  32006  hmoplin  32028  chirredlem1  32476  mdsymlem2  32490  foresf1o  32589  zarcls1  34029  ordtconnlem1  34084  signstfvn  34729  isbasisrelowllem1  37685  isbasisrelowllem2  37686  pibt2  37747  lindsadd  37948  lindsdom  37949  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem25  37980  poimirlem29  37984  heicant  37990  cnambfre  38003  itg2addnclem  38006  ftc1anclem5  38032  ftc1anc  38036  rrnequiv  38170  isfldidl  38403  ispridlc  38405  supxrgelem  45785  supminfxr  45910  uhgrimisgrgric  48419  cycl3grtri  48435  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  itcovalt2lem2  49164  reccot  50245  rectan  50246