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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  soltmin  6130  frfi  9298  wemappo  9568  iccsplit  13507  ccatswrd  14691  sqrmo  15275  pcdvdstr  16901  vdwlem12  17017  mreexexlem4d  17664  iscatd2  17698  oppccomfpropd  17744  resssetc  18110  resscatc  18127  mod1ile  18508  mod2ile  18509  prdssgrpd  18716  prdsmndd  18753  grprcan  18961  prdsrngd  20141  prdsringd  20286  lmodprop2d  20886  lssintcl  20926  prdslmodd  20931  islmhm2  21001  islbs3  21121  ofco2  22394  mdetmul  22566  restopnb  23118  regsep2  23319  iunconn  23371  blsscls2  24448  met2ndci  24466  xrsblre  24756  nosupbnd1lem5  27681  conway  27768  addsass  27969  mulscom  28099  legso  28583  colline  28633  tglowdim2ln  28635  cgrahl  28811  f1otrg  28855  f1otrge  28856  ax5seglem4  28916  ax5seglem5  28917  axcontlem4  28951  axcontlem8  28955  axcontlem9  28956  axcontlem10  28957  eengtrkg  28970  rusgrnumwwlks  29961  frgr3v  30261  lmhmimasvsca  33039  submomnd  33083  ogrpaddltbi  33091  erdszelem8  35225  elmrsubrn  35547  btwncomim  36036  btwnswapid  36040  broutsideof3  36149  outsideoftr  36152  outsidele  36155  isbasisrelowllem1  37378  isbasisrelowllem2  37379  cvrletrN  39296  ltltncvr  39447  atcvrj2b  39456  2at0mat0  39549  paddasslem11  39854  pmod1i  39872  lautcvr  40116  tendoplass  40807  tendodi1  40808  tendodi2  40809  cdlemk34  40934  mendassa  43189  grumnud  44285  3adantlr3  45044  ssinc  45091  ssdec  45092  ioondisj2  45502  ioondisj1  45503  subsubelfzo0  47335  ply1mulgsumlem2  48343  lincresunit3lem2  48436  catprs  48966  fthcomf  49077  oppcthinco  49305  oppcthinendcALT  49307