Theorem sylanl1 671

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

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  adantlll  710  adantllr  711  isocnv  6806  odi  7897  oeoelem  7916  mapxpen  8366  xadddilem  12369  pcqmul  15888  infpnlem1  15944  setsn0fun  16218  chpdmat  20971  neitr  21310  hausflimi  22109  nmoix  22858  nmoleub  22860  metdsre  22981  bncssbn  23497  usgr2edg1  26437  crctcshwlkn0  27064  sspphOLD  28227  unoplin  29296  hmoplin  29318  chirredlem1  29766  mdsymlem2  29780  foresf1o  29853  ordtconnlem1  30478  isbasisrelowllem1  33693  isbasisrelowllem2  33694  lindsdom  33884  matunitlindflem1  33886  matunitlindflem2  33887  poimirlem25  33915  poimirlem29  33919  heicant  33925  cnambfre  33938  itg2addnclem  33941  ftc1anclem5  33969  ftc1anc  33973  rrnequiv  34113  isfldidl  34346  ispridlc  34348  supxrgelem  40285  supminfxr  40425  reccot  43289  rectan  43290