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  7364  f1iun  7983  odi  8618  oeoelem  8638  mapxpen  9193  xadddilem  13454  hashgt23el  14599  pcqmul  17063  infpnlem1  17120  setsn0fun  17383  lindsdom  22189  matunitlindflem1  23027  matunitlindflem2  23028  chpdmat  23192  neitr  23531  hausflimi  24332  nmoix  25081  nmoleub  25083  metdsre  25206  bncssbn  25728  usgr2edg  29824  usgr2edg1  29826  crctcshwlkn0  30443  unoplin  32555  hmoplin  32577  chirredlem1  33025  mdsymlem2  33039  foresf1o  33175  zarcls1  34584  ordtconnlem1  34639  signstfvn  35281  isbasisrelowllem1  38483  isbasisrelowllem2  38484  pibt2  38545  lindsadd  38741  poimirlem25  38768  poimirlem29  38772  heicant  38778  cnambfre  38791  itg2addnclem  38794  ftc1anclem5  38820  ftc1anc  38824  rrnequiv  38972  isfldidl  39205  ispridlc  39207  supxrgelem  46564  supminfxr  46689  uhgrimisgrgric  49244  cycl3grtri  49260  gpg5nbgrvtx03star  49393  gpg5nbgr3star  49394  itcovalt2lem2  50003  reccot  51163  rectan  51164