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  7330  f1iun  7945  odi  8571  oeoelem  8591  mapxpen  9146  xadddilem  13405  hashgt23el  14549  pcqmul  17011  infpnlem1  17068  setsn0fun  17331  lindsdom  22136  matunitlindflem1  22974  matunitlindflem2  22975  chpdmat  23139  neitr  23478  hausflimi  24279  nmoix  25028  nmoleub  25030  metdsre  25153  bncssbn  25675  usgr2edg  29773  usgr2edg1  29775  crctcshwlkn0  30392  unoplin  32504  hmoplin  32526  chirredlem1  32974  mdsymlem2  32988  foresf1o  33082  zarcls1  34483  ordtconnlem1  34538  signstfvn  35181  isbasisrelowllem1  38246  isbasisrelowllem2  38247  pibt2  38308  lindsadd  38504  poimirlem25  38531  poimirlem29  38535  heicant  38541  cnambfre  38554  itg2addnclem  38557  ftc1anclem5  38583  ftc1anc  38587  rrnequiv  38737  isfldidl  38970  ispridlc  38972  supxrgelem  46293  supminfxr  46418  uhgrimisgrgric  48973  cycl3grtri  48989  gpg5nbgrvtx03star  49122  gpg5nbgr3star  49123  itcovalt2lem2  49732  reccot  50795  rectan  50796