Theorem simplr2 1214

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simplr2	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

Proof of Theorem simplr2

Step	Hyp	Ref	Expression
1		simp2 1135	. 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  pcdvdstr  16813  vdwlem12  16929  iscatd2  17629  oppccomfpropd  17677  resssetc  18046  resscatc  18063  mod1ile  18450  mod2ile  18451  prdssgrpd  18658  prdsmndd  18692  grprcan  18894  mulgnn0dir  19020  mulgnn0di  19734  mulgdi  19735  lmodprop2d  20678  lssintcl  20719  prdslmodd  20724  islmhm2  20793  islbs3  20913  mdetmul  22345  restopnb  22899  nrmsep  23081  iunconn  23152  ptpjopn  23336  blsscls2  24233  xrsblre  24547  icccmplem2  24559  icccvx  24695  conway  27537  addsass  27727  mulscom  27834  colline  28167  tglowdim2ln  28169  f1otrg  28389  f1otrge  28390  ax5seglem5  28458  axcontlem3  28491  axcontlem4  28492  axcontlem8  28496  eengtrkg  28511  2pthon3v  29464  erclwwlktr  29542  erclwwlkntr  29591  eucrctshift  29763  frgr3v  29795  frgr2wwlkeqm  29851  xrofsup  32247  lmhmimasvsca  32467  submomnd  32498  ogrpaddltbi  32506  erdszelem8  34487  cvmliftmolem2  34571  cvmlift2lem12  34603  btwnswapid  35293  btwnsegle  35393  broutsideof3  35402  outsidele  35408  isbasisrelowllem2  36540  cvrletrN  38446  ltltncvr  38597  atcvrj2b  38606  cvrat4  38617  2at0mat0  38699  islpln2a  38722  paddasslem11  39004  pmod1i  39022  lautcvr  39266  cdlemg4c  39786  tendoplass  39957  tendodi1  39958  tendodi2  39959  mendlmod  42237  mendassa  42238  3adantlr3  44026  ssinc  44077  ssdec  44078  ioondisj2  44504  ioondisj1  44505  stoweidlem60  45074  ply1mulgsumlem2  47155  lincresunit3lem2  47248  catprs  47718