Theorem simplr3 1218

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 1139	. 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  ttrclss  9715  ttrclselem2  9721  iccsplit  13462  ccatswrd  14618  pfxccat3  14684  modfsummods  15739  pcdvdstr  16809  vdwlem12  16925  cshwsidrepswmod0  17028  iscatd2  17625  oppccomfpropd  17673  initoeu2lem0  17963  resssetc  18042  resscatc  18059  yonedalem4c  18230  mod1ile  18446  mod2ile  18447  prdssgrpd  18624  prdsmndd  18658  grprcan  18858  mulgnn0dir  18984  mulgdir  18986  mulgass  18991  mulgnn0di  19693  mulgdi  19694  dprd2da  19912  lmodprop2d  20534  lssintcl  20575  prdslmodd  20580  islmhm2  20649  islbs2  20767  islbs3  20768  dmatmul  21999  mdetmul  22125  restopnb  22679  iunconn  22932  1stcelcls  22965  blsscls2  24013  stdbdbl  24026  xrsblre  24327  icccmplem2  24339  itg1val2  25201  cvxcl  26489  conway  27301  sleadd1  27475  addsass  27491  mulscom  27598  colline  27931  tglowdim2ln  27933  f1otrg  28153  f1otrge  28154  ax5seglem4  28221  ax5seglem5  28222  axcontlem3  28255  axcontlem8  28260  axcontlem9  28261  eengtrkg  28275  frgr3v  29559  xrofsup  32011  submomnd  32259  ogrpaddltbi  32267  erdszelem8  34220  resconn  34268  cvmliftmolem2  34304  cvmlift2lem12  34336  broutsideof3  35129  outsideoftr  35132  outsidele  35135  ltltncvr  38342  atcvrj2b  38351  cvrat4  38362  cvrat42  38363  2at0mat0  38444  islpln2a  38467  paddasslem11  38749  pmod1i  38767  lhpm0atN  38948  lautcvr  39011  cdlemg4c  39531  tendoplass  39702  tendodi1  39703  tendodi2  39704  dgrsub2  41925  grumnud  43093  ssinc  43824  ssdec  43825  ioondisj2  44254  ioondisj1  44255  ply1mulgsumlem2  47116  catprs  47679