Theorem sylanl1 680

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  adantlll  718  adantllr  719  adantl3r  750  isocnv  7305  f1iun  7922  odi  8543  oeoelem  8562  mapxpen  9107  xadddilem  13254  hashgt23el  14389  pcqmul  16824  infpnlem1  16881  setsn0fun  17143  chpdmat  22728  neitr  23067  hausflimi  23867  nmoix  24617  nmoleub  24619  metdsre  24742  bncssbn  25274  usgr2edg  29137  usgr2edg1  29139  crctcshwlkn0  29751  unoplin  31849  hmoplin  31871  chirredlem1  32319  mdsymlem2  32333  foresf1o  32433  zarcls1  33859  ordtconnlem1  33914  signstfvn  34560  isbasisrelowllem1  37343  isbasisrelowllem2  37344  pibt2  37405  lindsadd  37607  lindsdom  37608  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem25  37639  poimirlem29  37643  heicant  37649  cnambfre  37662  itg2addnclem  37665  ftc1anclem5  37691  ftc1anc  37695  rrnequiv  37829  isfldidl  38062  ispridlc  38064  supxrgelem  45333  supminfxr  45460  uhgrimisgrgric  47931  cycl3grtri  47946  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  itcovalt2lem2  48665  reccot  49747  rectan  49748