Theorem simplr3 1214

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  soltmin  6148  frfi  9322  wemappo  9592  ttrclss  9763  ttrclselem2  9769  iccsplit  13516  ccatswrd  14676  pfxccat3  14742  modfsummods  15797  pcdvdstr  16878  vdwlem12  16994  cshwsidrepswmod0  17097  iscatd2  17694  oppccomfpropd  17742  initoeu2lem0  18035  resssetc  18114  resscatc  18131  yonedalem4c  18302  mod1ile  18518  mod2ile  18519  prdssgrpd  18726  prdsmndd  18760  grprcan  18968  mulgnn0dir  19098  mulgdir  19100  mulgass  19105  mulgnn0di  19823  mulgdi  19824  dprd2da  20042  lmodprop2d  20900  lssintcl  20941  prdslmodd  20946  islmhm2  21016  islbs2  21135  islbs3  21136  dmatmul  22490  mdetmul  22616  restopnb  23170  iunconn  23423  1stcelcls  23456  blsscls2  24504  stdbdbl  24517  xrsblre  24818  icccmplem2  24830  itg1val2  25704  cvxcl  27013  conway  27829  sleadd1  28003  addsass  28019  mulscom  28140  colline  28576  tglowdim2ln  28578  f1otrg  28798  f1otrge  28799  ax5seglem4  28866  ax5seglem5  28867  axcontlem3  28900  axcontlem8  28905  axcontlem9  28906  eengtrkg  28920  frgr3v  30208  xrofsup  32671  lmhmimasvsca  32912  submomnd  32945  ogrpaddltbi  32953  erdszelem8  35026  resconn  35074  cvmliftmolem2  35110  cvmlift2lem12  35142  r1peuqusdeg1  35471  broutsideof3  35950  outsideoftr  35953  outsidele  35956  ltltncvr  39122  atcvrj2b  39131  cvrat4  39142  cvrat42  39143  2at0mat0  39224  islpln2a  39247  paddasslem11  39529  pmod1i  39547  lhpm0atN  39728  lautcvr  39791  cdlemg4c  40311  tendoplass  40482  tendodi1  40483  tendodi2  40484  dgrsub2  42796  grumnud  43960  ssinc  44688  ssdec  44689  ioondisj2  45111  ioondisj1  45112  ply1mulgsumlem2  47770  catprs  48332