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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  soltmin  6130  frfi  9298  wemappo  9568  ttrclss  9739  ttrclselem2  9745  iccsplit  13507  ccatswrd  14691  pfxccat3  14757  modfsummods  15814  pcdvdstr  16901  vdwlem12  17017  cshwsidrepswmod0  17119  iscatd2  17698  oppccomfpropd  17744  initoeu2lem0  18031  resssetc  18110  resscatc  18127  yonedalem4c  18294  mod1ile  18508  mod2ile  18509  prdssgrpd  18716  prdsmndd  18753  grprcan  18961  mulgnn0dir  19092  mulgdir  19094  mulgass  19099  mulgnn0di  19811  mulgdi  19812  dprd2da  20030  lmodprop2d  20886  lssintcl  20926  prdslmodd  20931  islmhm2  21001  islbs2  21120  islbs3  21121  dmatmul  22440  mdetmul  22566  restopnb  23118  iunconn  23371  1stcelcls  23404  blsscls2  24448  stdbdbl  24461  xrsblre  24756  icccmplem2  24768  itg1val2  25642  cvxcl  26952  conway  27768  sleadd1  27953  addsass  27969  mulscom  28099  colline  28633  tglowdim2ln  28635  f1otrg  28855  f1otrge  28856  ax5seglem4  28916  ax5seglem5  28917  axcontlem3  28950  axcontlem8  28955  axcontlem9  28956  eengtrkg  28970  frgr3v  30261  xrofsup  32749  lmhmimasvsca  33039  submomnd  33083  ogrpaddltbi  33091  erdszelem8  35225  resconn  35273  cvmliftmolem2  35309  cvmlift2lem12  35341  r1peuqusdeg1  35670  broutsideof3  36149  outsideoftr  36152  outsidele  36155  ltltncvr  39447  atcvrj2b  39456  cvrat4  39467  cvrat42  39468  2at0mat0  39549  islpln2a  39572  paddasslem11  39854  pmod1i  39872  lhpm0atN  40053  lautcvr  40116  cdlemg4c  40636  tendoplass  40807  tendodi1  40808  tendodi2  40809  dgrsub2  43126  grumnud  44277  ssinc  45078  ssdec  45079  ioondisj2  45489  ioondisj1  45490  ply1mulgsumlem2  48330  catprs  48953  fthcomf  49064  oppcthinco  49292  oppcthinendcALT  49294