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  7286  f1iun  7898  odi  8516  oeoelem  8536  mapxpen  9083  xadddilem  13221  hashgt23el  14359  pcqmul  16793  infpnlem1  16850  setsn0fun  17112  chpdmat  22797  neitr  23136  hausflimi  23936  nmoix  24685  nmoleub  24687  metdsre  24810  bncssbn  25342  usgr2edg  29295  usgr2edg1  29297  crctcshwlkn0  29906  unoplin  32007  hmoplin  32029  chirredlem1  32477  mdsymlem2  32491  foresf1o  32590  zarcls1  34046  ordtconnlem1  34101  signstfvn  34746  isbasisrelowllem1  37607  isbasisrelowllem2  37608  pibt2  37669  lindsadd  37861  lindsdom  37862  matunitlindflem1  37864  matunitlindflem2  37865  poimirlem25  37893  poimirlem29  37897  heicant  37903  cnambfre  37916  itg2addnclem  37919  ftc1anclem5  37945  ftc1anc  37949  rrnequiv  38083  isfldidl  38316  ispridlc  38318  supxrgelem  45693  supminfxr  45819  uhgrimisgrgric  48288  cycl3grtri  48304  gpg5nbgrvtx03star  48437  gpg5nbgr3star  48438  itcovalt2lem2  49033  reccot  50114  rectan  50115