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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  adantlll  716  adantllr  717  adantl3r  748  isocnv  7075  f1iun  7637  odi  8197  oeoelem  8216  mapxpen  8675  xadddilem  12679  hashgt23el  13777  pcqmul  16182  infpnlem1  16238  setsn0fun  16512  chpdmat  21441  neitr  21780  hausflimi  22580  nmoix  23330  nmoleub  23332  metdsre  23453  bncssbn  23969  usgr2edg  26984  usgr2edg1  26986  crctcshwlkn0  27591  unoplin  29689  hmoplin  29711  chirredlem1  30159  mdsymlem2  30173  foresf1o  30257  ordtconnlem1  31160  signstfvn  31832  isbasisrelowllem1  34628  isbasisrelowllem2  34629  pibt2  34690  lindsadd  34877  lindsdom  34878  matunitlindflem1  34880  matunitlindflem2  34881  poimirlem25  34909  poimirlem29  34913  heicant  34919  cnambfre  34932  itg2addnclem  34935  ftc1anclem5  34963  ftc1anc  34967  rrnequiv  35105  isfldidl  35338  ispridlc  35340  supxrgelem  41595  supminfxr  41730  reccot  44848  rectan  44849