Theorem sylanl1 693

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  adantlll  731  adantllr  732  adantl3r  763  isocnv  7339  f1iun  7950  odi  8573  oeoelem  8593  mapxpen  9141  xadddilem  13338  hashgt23el  14481  pcqmul  16938  infpnlem1  16995  setsn0fun  17258  chpdmat  23035  neitr  23374  hausflimi  24174  nmoix  24923  nmoleub  24925  metdsre  25048  bncssbn  25570  usgr2edg  29597  usgr2edg1  29599  crctcshwlkn0  30207  unoplin  32309  hmoplin  32331  chirredlem1  32779  mdsymlem2  32793  foresf1o  32887  zarcls1  34290  ordtconnlem1  34345  signstfvn  34988  isbasisrelowllem1  38042  isbasisrelowllem2  38043  pibt2  38104  lindsadd  38305  lindsdom  38306  matunitlindflem1  38308  matunitlindflem2  38309  poimirlem25  38337  poimirlem29  38341  heicant  38347  cnambfre  38360  itg2addnclem  38363  ftc1anclem5  38389  ftc1anc  38393  rrnequiv  38527  isfldidl  38760  ispridlc  38762  supxrgelem  46094  supminfxr  46219  uhgrimisgrgric  48737  cycl3grtri  48753  gpg5nbgrvtx03star  48886  gpg5nbgr3star  48887  itcovalt2lem2  49497  reccot  50577  rectan  50578