Theorem simplr2 1218

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 728	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  soltmin  6093  frfi  9188  wemappo  9457  iccsplit  13429  ccatswrd  14622  pcdvdstr  16838  vdwlem12  16954  iscatd2  17638  oppccomfpropd  17684  resssetc  18050  resscatc  18067  mod1ile  18450  mod2ile  18451  prdssgrpd  18692  prdsmndd  18729  grprcan  18940  mulgnn0dir  19071  mulgnn0di  19791  mulgdi  19792  submomnd  20098  ogrpaddltbi  20105  lmodprop2d  20910  lssintcl  20950  prdslmodd  20955  islmhm2  21025  islbs3  21145  mdetmul  22598  restopnb  23150  nrmsep  23332  iunconn  23403  ptpjopn  23587  blsscls2  24479  xrsblre  24787  icccmplem2  24799  icccvx  24927  conway  27785  addsass  28011  mulscom  28145  addonbday  28285  colline  28731  tglowdim2ln  28733  f1otrg  28953  f1otrge  28954  ax5seglem5  29016  axcontlem3  29049  axcontlem4  29050  axcontlem8  29054  eengtrkg  29069  2pthon3v  30026  erclwwlktr  30107  erclwwlkntr  30156  eucrctshift  30328  frgr3v  30360  frgr2wwlkeqm  30416  xrofsup  32855  lmhmimasvsca  33114  erdszelem8  35396  cvmliftmolem2  35480  cvmlift2lem12  35512  r1peuqusdeg1  35841  btwnswapid  36215  btwnsegle  36315  broutsideof3  36324  outsidele  36330  isbasisrelowllem2  37686  cvrletrN  39733  ltltncvr  39883  atcvrj2b  39892  cvrat4  39903  2at0mat0  39985  islpln2a  40008  paddasslem11  40290  pmod1i  40308  lautcvr  40552  cdlemg4c  41072  tendoplass  41243  tendodi1  41244  tendodi2  41245  mendlmod  43635  mendassa  43636  3adantlr3  45489  ssinc  45535  ssdec  45536  ioondisj2  45941  ioondisj1  45942  stoweidlem60  46506  ply1mulgsumlem2  48875  lincresunit3lem2  48968  catprs  49498  fthcomf  49644  oppcthinco  49926  oppcthinendcALT  49928