Theorem simplr1 1222

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  soltmin  6093  frfi  9192  wemappo  9461  iccsplit  13436  ccatswrd  14629  sqrmo  15211  pcdvdstr  16845  vdwlem12  16961  mreexexlem4d  17611  iscatd2  17645  oppccomfpropd  17691  resssetc  18057  resscatc  18074  mod1ile  18457  mod2ile  18458  prdssgrpd  18699  prdsmndd  18736  grprcan  18947  submomnd  20105  ogrpaddltbi  20112  prdsrngd  20155  prdsringd  20298  lmodprop2d  20921  lssintcl  20961  prdslmodd  20966  islmhm2  21035  islbs3  21155  ofco2  22441  mdetmul  22613  restopnb  23165  regsep2  23366  iunconn  23418  blsscls2  24494  met2ndci  24512  xrsblre  24802  nosupbnd1lem5  27701  conway  27796  addsass  28022  mulscom  28156  legso  28692  colline  28742  tglowdim2ln  28744  cgrahl  28920  f1otrg  28964  f1otrge  28965  ax5seglem4  29026  ax5seglem5  29027  axcontlem4  29061  axcontlem8  29065  axcontlem9  29066  axcontlem10  29067  eengtrkg  29080  rusgrnumwwlks  30070  frgr3v  30370  lmhmimasvsca  33125  erdszelem8  35433  elmrsubrn  35755  btwncomim  36248  btwnswapid  36252  broutsideof3  36361  outsideoftr  36364  outsidele  36367  isbasisrelowllem1  37724  isbasisrelowllem2  37725  cvrletrN  39772  ltltncvr  39922  atcvrj2b  39931  2at0mat0  40024  paddasslem11  40329  pmod1i  40347  lautcvr  40591  tendoplass  41282  tendodi1  41283  tendodi2  41284  cdlemk34  41409  mendassa  43642  grumnud  44737  3adantlr3  45495  ssinc  45541  ssdec  45542  ioondisj2  45945  ioondisj1  45946  subsubelfzo0  47797  ply1mulgsumlem2  48885  lincresunit3lem2  48978  catprs  49508  fthcomf  49654  oppcthinco  49936  oppcthinendcALT  49938