Theorem simplr2 1217

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  soltmin  6138  frfi  9288  wemappo  9544  iccsplit  13462  ccatswrd  14618  pcdvdstr  16809  vdwlem12  16925  iscatd2  17625  oppccomfpropd  17673  resssetc  18042  resscatc  18059  mod1ile  18446  mod2ile  18447  prdssgrpd  18624  prdsmndd  18658  grprcan  18858  mulgnn0dir  18984  mulgnn0di  19693  mulgdi  19694  lmodprop2d  20534  lssintcl  20575  prdslmodd  20580  islmhm2  20649  islbs3  20768  mdetmul  22125  restopnb  22679  nrmsep  22861  iunconn  22932  ptpjopn  23116  blsscls2  24013  xrsblre  24327  icccmplem2  24339  icccvx  24466  conway  27300  addsass  27488  mulscom  27595  colline  27900  tglowdim2ln  27902  f1otrg  28122  f1otrge  28123  ax5seglem5  28191  axcontlem3  28224  axcontlem4  28225  axcontlem8  28229  eengtrkg  28244  2pthon3v  29197  erclwwlktr  29275  erclwwlkntr  29324  eucrctshift  29496  frgr3v  29528  frgr2wwlkeqm  29584  xrofsup  31980  submomnd  32228  ogrpaddltbi  32236  erdszelem8  34189  cvmliftmolem2  34273  cvmlift2lem12  34305  btwnswapid  34989  btwnsegle  35089  broutsideof3  35098  outsidele  35104  isbasisrelowllem2  36237  cvrletrN  38143  ltltncvr  38294  atcvrj2b  38303  cvrat4  38314  2at0mat0  38396  islpln2a  38419  paddasslem11  38701  pmod1i  38719  lautcvr  38963  cdlemg4c  39483  tendoplass  39654  tendodi1  39655  tendodi2  39656  mendlmod  41935  mendassa  41936  3adantlr3  43724  ssinc  43776  ssdec  43777  ioondisj2  44206  ioondisj1  44207  stoweidlem60  44776  ply1mulgsumlem2  47068  lincresunit3lem2  47161  catprs  47631