Theorem simplr1 1212

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

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

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 1086

This theorem is referenced by:  soltmin  6140  frfi  9315  wemappo  9585  iccsplit  13510  ccatswrd  14671  sqrmo  15251  pcdvdstr  16873  vdwlem12  16989  mreexexlem4d  17655  iscatd2  17689  oppccomfpropd  17737  resssetc  18109  resscatc  18126  mod1ile  18513  mod2ile  18514  prdssgrpd  18721  prdsmndd  18755  grprcan  18963  prdsrngd  20155  prdsringd  20296  lmodprop2d  20896  lssintcl  20937  prdslmodd  20942  islmhm2  21012  islbs3  21132  ofco2  22441  mdetmul  22613  restopnb  23167  regsep2  23368  iunconn  23420  blsscls2  24501  met2ndci  24519  xrsblre  24815  nosupbnd1lem5  27739  conway  27826  addsass  28016  mulscom  28137  legso  28523  colline  28573  tglowdim2ln  28575  cgrahl  28751  f1otrg  28795  f1otrge  28796  ax5seglem4  28863  ax5seglem5  28864  axcontlem4  28898  axcontlem8  28902  axcontlem9  28903  axcontlem10  28904  eengtrkg  28917  rusgrnumwwlks  29905  frgr3v  30205  lmhmimasvsca  32915  submomnd  32949  ogrpaddltbi  32957  erdszelem8  35039  elmrsubrn  35361  btwncomim  35850  btwnswapid  35854  broutsideof3  35963  outsideoftr  35966  outsidele  35969  isbasisrelowllem1  37075  isbasisrelowllem2  37076  cvrletrN  38984  ltltncvr  39135  atcvrj2b  39144  2at0mat0  39237  paddasslem11  39542  pmod1i  39560  lautcvr  39804  tendoplass  40495  tendodi1  40496  tendodi2  40497  cdlemk34  40622  mendassa  42892  grumnud  43997  3adantlr3  44676  ssinc  44725  ssdec  44726  ioondisj2  45147  ioondisj1  45148  subsubelfzo0  46975  ply1mulgsumlem2  47806  lincresunit3lem2  47899  catprs  48368