Theorem simplr1 1276

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simplr1	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Proof of Theorem simplr1

Step	Hyp	Ref	Expression
1		simp1 1167	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antlr 719	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  soltmin  5749  frfi  8446  wemappo  8695  iccsplit  12556  ccatswrd  13707  sqrmo  14330  pcdvdstr  15910  vdwlem12  16026  mreexexlem4d  16619  iscatd2  16653  oppccomfpropd  16698  resssetc  17053  resscatc  17066  mod1ile  17417  mod2ile  17418  prdsmndd  17635  grprcan  17768  prdsringd  18925  lmodprop2d  19240  lssintcl  19282  prdslmodd  19287  islmhm2  19356  islbs3  19475  ofco2  20580  mdetmul  20752  restopnb  21305  regsep2  21506  iunconn  21557  blsscls2  22634  met2ndci  22652  xrsblre  22939  legso  25843  colline  25893  tglowdim2ln  25895  cgrahl  26067  f1otrg  26101  f1otrge  26102  ax5seglem4  26162  ax5seglem5  26163  axcontlem4  26197  axcontlem8  26201  axcontlem9  26202  axcontlem10  26203  eengtrkg  26215  rusgrnumwwlks  27258  rusgrnumwwlksOLD  27259  frgr3v  27617  submomnd  30219  ogrpaddltbi  30228  erdszelem8  31690  nosupbnd1lem5  32364  conway  32416  btwncomim  32626  btwnswapid  32630  broutsideof3  32739  outsideoftr  32742  outsidele  32745  isbasisrelowllem1  33694  isbasisrelowllem2  33695  cvrletrN  35287  ltltncvr  35437  atcvrj2b  35446  2at0mat0  35539  paddasslem11  35844  pmod1i  35862  lautcvr  36106  tendoplass  36797  tendodi1  36798  tendodi2  36799  cdlemk34  36924  mendassa  38538  3adantlr3  39949  ssinc  40012  ssdec  40013  ioondisj2  40451  ioondisj1  40452  subsubelfzo0  42165  ply1mulgsumlem2  42963  lincresunit3lem2  43057