Theorem simplr1 1216

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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antlr 726	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  soltmin  6138  frfi  9288  wemappo  9544  iccsplit  13462  ccatswrd  14618  sqrmo  15198  pcdvdstr  16809  vdwlem12  16925  mreexexlem4d  17591  iscatd2  17625  oppccomfpropd  17673  resssetc  18042  resscatc  18059  mod1ile  18446  mod2ile  18447  prdssgrpd  18624  prdsmndd  18658  grprcan  18858  prdsringd  20134  lmodprop2d  20534  lssintcl  20575  prdslmodd  20580  islmhm2  20649  islbs3  20768  ofco2  21953  mdetmul  22125  restopnb  22679  regsep2  22880  iunconn  22932  blsscls2  24013  met2ndci  24031  xrsblre  24327  nosupbnd1lem5  27215  conway  27300  addsass  27488  mulscom  27595  legso  27850  colline  27900  tglowdim2ln  27902  cgrahl  28078  f1otrg  28122  f1otrge  28123  ax5seglem4  28190  ax5seglem5  28191  axcontlem4  28225  axcontlem8  28229  axcontlem9  28230  axcontlem10  28231  eengtrkg  28244  rusgrnumwwlks  29228  frgr3v  29528  submomnd  32228  ogrpaddltbi  32236  erdszelem8  34189  elmrsubrn  34511  btwncomim  34985  btwnswapid  34989  broutsideof3  35098  outsideoftr  35101  outsidele  35104  isbasisrelowllem1  36236  isbasisrelowllem2  36237  cvrletrN  38143  ltltncvr  38294  atcvrj2b  38303  2at0mat0  38396  paddasslem11  38701  pmod1i  38719  lautcvr  38963  tendoplass  39654  tendodi1  39655  tendodi2  39656  cdlemk34  39781  mendassa  41936  grumnud  43045  3adantlr3  43724  ssinc  43776  ssdec  43777  ioondisj2  44206  ioondisj1  44207  subsubelfzo0  46034  prdsrngd  46677  ply1mulgsumlem2  47068  lincresunit3lem2  47161  catprs  47631