Theorem sylanl1 678

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 396

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 206  df-an 397

This theorem is referenced by:  adantlll  716  adantllr  717  adantl3r  748  isocnv  7323  f1iun  7926  odi  8575  oeoelem  8594  mapxpen  9139  xadddilem  13269  hashgt23el  14380  pcqmul  16782  infpnlem1  16839  setsn0fun  17102  chpdmat  22334  neitr  22675  hausflimi  23475  nmoix  24237  nmoleub  24239  metdsre  24360  bncssbn  24882  usgr2edg  28456  usgr2edg1  28458  crctcshwlkn0  29064  unoplin  31160  hmoplin  31182  chirredlem1  31630  mdsymlem2  31644  foresf1o  31729  zarcls1  32837  ordtconnlem1  32892  signstfvn  33568  isbasisrelowllem1  36224  isbasisrelowllem2  36225  pibt2  36286  lindsadd  36469  lindsdom  36470  matunitlindflem1  36472  matunitlindflem2  36473  poimirlem25  36501  poimirlem29  36505  heicant  36511  cnambfre  36524  itg2addnclem  36527  ftc1anclem5  36553  ftc1anc  36557  rrnequiv  36691  isfldidl  36924  ispridlc  36926  supxrgelem  44033  supminfxr  44160  itcovalt2lem2  47315  reccot  47756  rectan  47757