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  7323  f1iun  7942  odi  8591  oeoelem  8610  mapxpen  9157  xadddilem  13310  hashgt23el  14442  pcqmul  16873  infpnlem1  16930  setsn0fun  17192  chpdmat  22779  neitr  23118  hausflimi  23918  nmoix  24668  nmoleub  24670  metdsre  24793  bncssbn  25326  usgr2edg  29189  usgr2edg1  29191  crctcshwlkn0  29803  unoplin  31901  hmoplin  31923  chirredlem1  32371  mdsymlem2  32385  foresf1o  32485  zarcls1  33900  ordtconnlem1  33955  signstfvn  34601  isbasisrelowllem1  37373  isbasisrelowllem2  37374  pibt2  37435  lindsadd  37637  lindsdom  37638  matunitlindflem1  37640  matunitlindflem2  37641  poimirlem25  37669  poimirlem29  37673  heicant  37679  cnambfre  37692  itg2addnclem  37695  ftc1anclem5  37721  ftc1anc  37725  rrnequiv  37859  isfldidl  38092  ispridlc  38094  supxrgelem  45364  supminfxr  45491  uhgrimisgrgric  47944  cycl3grtri  47959  gpg5nbgrvtx03star  48082  gpg5nbgr3star  48083  itcovalt2lem2  48656  reccot  49622  rectan  49623