Theorem simplr3 1219

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 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  ttrclss  9632  ttrclselem2  9638  iccsplit  13429  ccatswrd  14622  pfxccat3  14687  modfsummods  15747  pcdvdstr  16838  vdwlem12  16954  cshwsidrepswmod0  17056  iscatd2  17638  oppccomfpropd  17684  initoeu2lem0  17971  resssetc  18050  resscatc  18067  yonedalem4c  18234  mod1ile  18450  mod2ile  18451  prdssgrpd  18692  prdsmndd  18729  grprcan  18940  mulgnn0dir  19071  mulgdir  19073  mulgass  19078  mulgnn0di  19791  mulgdi  19792  dprd2da  20010  submomnd  20098  ogrpaddltbi  20105  lmodprop2d  20910  lssintcl  20950  prdslmodd  20955  islmhm2  21025  islbs2  21144  islbs3  21145  dmatmul  22472  mdetmul  22598  restopnb  23150  iunconn  23403  1stcelcls  23436  blsscls2  24479  stdbdbl  24492  xrsblre  24787  icccmplem2  24799  itg1val2  25661  cvxcl  26962  conway  27785  leadds1  27995  addsass  28011  mulscom  28145  addonbday  28285  colline  28731  tglowdim2ln  28733  f1otrg  28953  f1otrge  28954  ax5seglem4  29015  ax5seglem5  29016  axcontlem3  29049  axcontlem8  29054  axcontlem9  29055  eengtrkg  29069  frgr3v  30360  xrofsup  32855  lmhmimasvsca  33114  erdszelem8  35396  resconn  35444  cvmliftmolem2  35480  cvmlift2lem12  35512  r1peuqusdeg1  35841  broutsideof3  36324  outsideoftr  36327  outsidele  36330  ltltncvr  39883  atcvrj2b  39892  cvrat4  39903  cvrat42  39904  2at0mat0  39985  islpln2a  40008  paddasslem11  40290  pmod1i  40308  lhpm0atN  40489  lautcvr  40552  cdlemg4c  41072  tendoplass  41243  tendodi1  41244  tendodi2  41245  dgrsub2  43581  grumnud  44731  ssinc  45535  ssdec  45536  ioondisj2  45941  ioondisj1  45942  ply1mulgsumlem2  48875  catprs  49498  fthcomf  49644  oppcthinco  49926  oppcthinendcALT  49928