Theorem simplr3 1265

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

Assertion

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

Proof of Theorem simplr3

Step	Hyp	Ref	Expression
1		simp3 1133	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 765	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  soltmin  5690  frfi  8370  wemappo  8619  iccsplit  12498  ccatswrd  13656  swrdccat3  13692  modfsummods  14724  pcdvdstr  15782  vdwlem12  15898  cshwsidrepswmod0  16003  iscatd2  16543  oppccomfpropd  16588  initoeu2lem0  16864  resssetc  16943  resscatc  16956  yonedalem4c  17118  mod1ile  17306  mod2ile  17307  prdsmndd  17524  grprcan  17656  mulgnn0dir  17772  mulgdir  17774  mulgass  17780  mulgnn0di  18431  mulgdi  18432  dprd2da  18641  lmodprop2d  19127  lssintcl  19166  prdslmodd  19171  islmhm2  19240  islbs2  19356  islbs3  19357  dmatmul  20505  mdetmul  20631  restopnb  21181  iunconn  21433  1stcelcls  21466  blsscls2  22510  stdbdbl  22523  xrsblre  22815  icccmplem2  22827  itg1val2  23650  cvxcl  24910  colline  25743  tglowdim2ln  25745  f1otrg  25950  f1otrge  25951  ax5seglem4  26011  ax5seglem5  26012  axcontlem3  26045  axcontlem8  26050  axcontlem9  26051  eengtrkg  26064  frgr3v  27429  xrofsup  29842  submomnd  30019  ogrpaddltbi  30028  erdszelem8  31487  resconn  31535  cvmliftmolem2  31571  cvmlift2lem12  31603  conway  32216  broutsideof3  32539  outsideoftr  32542  outsidele  32545  ltltncvr  35212  atcvrj2b  35221  cvrat4  35232  cvrat42  35233  2at0mat0  35314  islpln2a  35337  paddasslem11  35619  pmod1i  35637  lhpm0atN  35818  lautcvr  35881  cdlemg4c  36402  tendoplass  36573  tendodi1  36574  tendodi2  36575  dgrsub2  38207  ssinc  39763  ssdec  39764  ioondisj2  40217  ioondisj1  40218  pfxccat3  41936  ply1mulgsumlem2  42685