Theorem simplr2 1212

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soltmin  5998  frfi  8765  wemappo  9015  iccsplit  12874  ccatswrd  14032  pcdvdstr  16214  vdwlem12  16330  iscatd2  16954  oppccomfpropd  16999  resssetc  17354  resscatc  17367  mod1ile  17717  mod2ile  17718  prdsmndd  17946  grprcan  18139  mulgnn0dir  18259  mulgnn0di  18948  mulgdi  18949  lmodprop2d  19698  lssintcl  19738  prdslmodd  19743  islmhm2  19812  islbs3  19929  mdetmul  21234  restopnb  21785  nrmsep  21967  iunconn  22038  ptpjopn  22222  blsscls2  23116  xrsblre  23421  icccmplem2  23433  icccvx  23556  colline  26437  tglowdim2ln  26439  f1otrg  26659  f1otrge  26660  ax5seglem5  26721  axcontlem3  26754  axcontlem4  26755  axcontlem8  26759  eengtrkg  26774  2pthon3v  27724  erclwwlktr  27802  erclwwlkntr  27852  eucrctshift  28024  frgr3v  28056  frgr2wwlkeqm  28112  xrofsup  30494  submomnd  30713  ogrpaddltbi  30721  erdszelem8  32447  cvmliftmolem2  32531  cvmlift2lem12  32563  conway  33266  btwnswapid  33480  btwnsegle  33580  broutsideof3  33589  outsidele  33595  isbasisrelowllem2  34639  cvrletrN  36411  ltltncvr  36561  atcvrj2b  36570  cvrat4  36581  2at0mat0  36663  islpln2a  36686  paddasslem11  36968  pmod1i  36986  lautcvr  37230  cdlemg4c  37750  tendoplass  37921  tendodi1  37922  tendodi2  37923  mendlmod  39800  mendassa  39801  3adantlr3  41305  ssinc  41360  ssdec  41361  ioondisj2  41774  ioondisj1  41775  stoweidlem60  42352  ply1mulgsumlem2  44448  lincresunit3lem2  44542