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

This theorem is referenced by:  soltmin  6038  frfi  9020  wemappo  9269  iccsplit  13199  ccatswrd  14362  sqrmo  14944  pcdvdstr  16558  vdwlem12  16674  mreexexlem4d  17337  iscatd2  17371  oppccomfpropd  17419  resssetc  17788  resscatc  17805  mod1ile  18192  mod2ile  18193  prdsmndd  18399  grprcan  18594  prdsringd  19832  lmodprop2d  20166  lssintcl  20207  prdslmodd  20212  islmhm2  20281  islbs3  20398  ofco2  21581  mdetmul  21753  restopnb  22307  regsep2  22508  iunconn  22560  blsscls2  23641  met2ndci  23659  xrsblre  23955  legso  26941  colline  26991  tglowdim2ln  26993  cgrahl  27169  f1otrg  27213  f1otrge  27214  ax5seglem4  27281  ax5seglem5  27282  axcontlem4  27316  axcontlem8  27320  axcontlem9  27321  axcontlem10  27322  eengtrkg  27335  rusgrnumwwlks  28318  frgr3v  28618  submomnd  31315  ogrpaddltbi  31323  erdszelem8  33139  elmrsubrn  33461  nosupbnd1lem5  33894  conway  33972  btwncomim  34294  btwnswapid  34298  broutsideof3  34407  outsideoftr  34410  outsidele  34413  isbasisrelowllem1  35505  isbasisrelowllem2  35506  cvrletrN  37266  ltltncvr  37416  atcvrj2b  37425  2at0mat0  37518  paddasslem11  37823  pmod1i  37841  lautcvr  38085  tendoplass  38776  tendodi1  38777  tendodi2  38778  cdlemk34  38903  mendassa  40999  grumnud  41857  3adantlr3  42537  ssinc  42590  ssdec  42591  ioondisj2  42985  ioondisj1  42986  subsubelfzo0  44770  ply1mulgsumlem2  45680  lincresunit3lem2  45773  catprs  46244