Theorem simplr1 1213

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  soltmin  6136  frfi  9290  wemappo  9546  iccsplit  13466  ccatswrd  14622  sqrmo  15202  pcdvdstr  16813  vdwlem12  16929  mreexexlem4d  17595  iscatd2  17629  oppccomfpropd  17677  resssetc  18046  resscatc  18063  mod1ile  18450  mod2ile  18451  prdssgrpd  18658  prdsmndd  18692  grprcan  18894  prdsrngd  20070  prdsringd  20209  lmodprop2d  20678  lssintcl  20719  prdslmodd  20724  islmhm2  20793  islbs3  20913  ofco2  22173  mdetmul  22345  restopnb  22899  regsep2  23100  iunconn  23152  blsscls2  24233  met2ndci  24251  xrsblre  24547  nosupbnd1lem5  27451  conway  27537  addsass  27727  mulscom  27834  legso  28117  colline  28167  tglowdim2ln  28169  cgrahl  28345  f1otrg  28389  f1otrge  28390  ax5seglem4  28457  ax5seglem5  28458  axcontlem4  28492  axcontlem8  28496  axcontlem9  28497  axcontlem10  28498  eengtrkg  28511  rusgrnumwwlks  29495  frgr3v  29795  lmhmimasvsca  32467  submomnd  32498  ogrpaddltbi  32506  erdszelem8  34487  elmrsubrn  34809  btwncomim  35289  btwnswapid  35293  broutsideof3  35402  outsideoftr  35405  outsidele  35408  isbasisrelowllem1  36539  isbasisrelowllem2  36540  cvrletrN  38446  ltltncvr  38597  atcvrj2b  38606  2at0mat0  38699  paddasslem11  39004  pmod1i  39022  lautcvr  39266  tendoplass  39957  tendodi1  39958  tendodi2  39959  cdlemk34  40084  mendassa  42238  grumnud  43347  3adantlr3  44026  ssinc  44077  ssdec  44078  ioondisj2  44504  ioondisj1  44505  subsubelfzo0  46332  ply1mulgsumlem2  47155  lincresunit3lem2  47248  catprs  47718