Theorem sylanl1 681

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 616	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 581	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  719  adantllr  720  adantl3r  751  isocnv  7285  f1iun  7897  odi  8514  oeoelem  8534  mapxpen  9081  xadddilem  13246  hashgt23el  14386  pcqmul  16824  infpnlem1  16881  setsn0fun  17143  chpdmat  22806  neitr  23145  hausflimi  23945  nmoix  24694  nmoleub  24696  metdsre  24819  bncssbn  25341  usgr2edg  29279  usgr2edg1  29281  crctcshwlkn0  29889  unoplin  31991  hmoplin  32013  chirredlem1  32461  mdsymlem2  32475  foresf1o  32574  zarcls1  34013  ordtconnlem1  34068  signstfvn  34713  isbasisrelowllem1  37671  isbasisrelowllem2  37672  pibt2  37733  lindsadd  37934  lindsdom  37935  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem25  37966  poimirlem29  37970  heicant  37976  cnambfre  37989  itg2addnclem  37992  ftc1anclem5  38018  ftc1anc  38022  rrnequiv  38156  isfldidl  38389  ispridlc  38391  supxrgelem  45767  supminfxr  45892  uhgrimisgrgric  48407  cycl3grtri  48423  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  itcovalt2lem2  49152  reccot  50233  rectan  50234