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  7957  odi  8591  oeoelem  8611  mapxpen  9166  xadddilem  13428  hashgt23el  14573  pcqmul  17037  infpnlem1  17094  setsn0fun  17357  lindsdom  22162  matunitlindflem1  23000  matunitlindflem2  23001  chpdmat  23165  neitr  23504  hausflimi  24305  nmoix  25054  nmoleub  25056  metdsre  25179  bncssbn  25701  usgr2edg  29797  usgr2edg1  29799  crctcshwlkn0  30416  unoplin  32528  hmoplin  32550  chirredlem1  32998  mdsymlem2  33012  foresf1o  33148  zarcls1  34548  ordtconnlem1  34603  signstfvn  35245  isbasisrelowllem1  38372  isbasisrelowllem2  38373  pibt2  38434  lindsadd  38630  poimirlem25  38657  poimirlem29  38661  heicant  38667  cnambfre  38680  itg2addnclem  38683  ftc1anclem5  38709  ftc1anc  38713  rrnequiv  38863  isfldidl  39096  ispridlc  39098  supxrgelem  46443  supminfxr  46568  uhgrimisgrgric  49123  cycl3grtri  49139  gpg5nbgrvtx03star  49272  gpg5nbgr3star  49273  itcovalt2lem2  49882  reccot  51020  rectan  51021