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  6129  frfi  9276  wemappo  9531  iccsplit  13449  ccatswrd  14605  pcdvdstr  16796  vdwlem12  16912  iscatd2  17612  oppccomfpropd  17660  resssetc  18029  resscatc  18046  mod1ile  18433  mod2ile  18434  prdssgrpd  18611  prdsmndd  18645  grprcan  18845  mulgnn0dir  18969  mulgnn0di  19676  mulgdi  19677  lmodprop2d  20511  lssintcl  20552  prdslmodd  20557  islmhm2  20626  islbs3  20745  mdetmul  22094  restopnb  22648  nrmsep  22830  iunconn  22901  ptpjopn  23085  blsscls2  23982  xrsblre  24296  icccmplem2  24308  icccvx  24435  conway  27267  addsass  27455  mulscom  27562  colline  27867  tglowdim2ln  27869  f1otrg  28089  f1otrge  28090  ax5seglem5  28158  axcontlem3  28191  axcontlem4  28192  axcontlem8  28196  eengtrkg  28211  2pthon3v  29164  erclwwlktr  29242  erclwwlkntr  29291  eucrctshift  29463  frgr3v  29495  frgr2wwlkeqm  29551  xrofsup  31951  submomnd  32199  ogrpaddltbi  32207  erdszelem8  34120  cvmliftmolem2  34204  cvmlift2lem12  34236  btwnswapid  34920  btwnsegle  35020  broutsideof3  35029  outsidele  35035  isbasisrelowllem2  36142  cvrletrN  38049  ltltncvr  38200  atcvrj2b  38209  cvrat4  38220  2at0mat0  38302  islpln2a  38325  paddasslem11  38607  pmod1i  38625  lautcvr  38869  cdlemg4c  39389  tendoplass  39560  tendodi1  39561  tendodi2  39562  mendlmod  41806  mendassa  41807  3adantlr3  43595  ssinc  43647  ssdec  43648  ioondisj2  44079  ioondisj1  44080  stoweidlem60  44649  ply1mulgsumlem2  46908  lincresunit3lem2  47001  catprs  47471