Theorem simplr3 1213

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soltmin  5995  frfi  8762  wemappo  9012  iccsplit  12870  ccatswrd  14029  pfxccat3  14095  modfsummods  15147  pcdvdstr  16211  vdwlem12  16327  cshwsidrepswmod0  16427  iscatd2  16951  oppccomfpropd  16996  initoeu2lem0  17272  resssetc  17351  resscatc  17364  yonedalem4c  17526  mod1ile  17714  mod2ile  17715  prdsmndd  17943  grprcan  18136  mulgnn0dir  18256  mulgdir  18258  mulgass  18263  mulgnn0di  18945  mulgdi  18946  dprd2da  19163  lmodprop2d  19695  lssintcl  19735  prdslmodd  19740  islmhm2  19809  islbs2  19925  islbs3  19926  dmatmul  21105  mdetmul  21231  restopnb  21782  iunconn  22035  1stcelcls  22068  blsscls2  23113  stdbdbl  23126  xrsblre  23418  icccmplem2  23430  itg1val2  24284  cvxcl  25561  colline  26434  tglowdim2ln  26436  f1otrg  26656  f1otrge  26657  ax5seglem4  26717  ax5seglem5  26718  axcontlem3  26751  axcontlem8  26756  axcontlem9  26757  eengtrkg  26771  frgr3v  28053  xrofsup  30491  submomnd  30711  ogrpaddltbi  30719  erdszelem8  32445  resconn  32493  cvmliftmolem2  32529  cvmlift2lem12  32561  conway  33264  broutsideof3  33587  outsideoftr  33590  outsidele  33593  ltltncvr  36558  atcvrj2b  36567  cvrat4  36578  cvrat42  36579  2at0mat0  36660  islpln2a  36683  paddasslem11  36965  pmod1i  36983  lhpm0atN  37164  lautcvr  37227  cdlemg4c  37747  tendoplass  37918  tendodi1  37919  tendodi2  37920  dgrsub2  39733  grumnud  40620  ssinc  41351  ssdec  41352  ioondisj2  41765  ioondisj1  41766  ply1mulgsumlem2  44440