Theorem simplr3 1224

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  soltmin  6093  frfi  9192  wemappo  9461  ttrclss  9639  ttrclselem2  9645  iccsplit  13436  ccatswrd  14629  pfxccat3  14694  modfsummods  15754  pcdvdstr  16845  vdwlem12  16961  cshwsidrepswmod0  17063  iscatd2  17645  oppccomfpropd  17691  initoeu2lem0  17978  resssetc  18057  resscatc  18074  yonedalem4c  18241  mod1ile  18457  mod2ile  18458  prdssgrpd  18699  prdsmndd  18736  grprcan  18947  mulgnn0dir  19078  mulgdir  19080  mulgass  19085  mulgnn0di  19798  mulgdi  19799  dprd2da  20017  submomnd  20105  ogrpaddltbi  20112  lmodprop2d  20921  lssintcl  20961  prdslmodd  20966  islmhm2  21035  islbs2  21154  islbs3  21155  dmatmul  22487  mdetmul  22613  restopnb  23165  iunconn  23418  1stcelcls  23451  blsscls2  24494  stdbdbl  24507  xrsblre  24802  icccmplem2  24814  itg1val2  25676  cvxcl  26973  conway  27796  leadds1  28006  addsass  28022  mulscom  28156  addonbday  28296  colline  28742  tglowdim2ln  28744  f1otrg  28964  f1otrge  28965  ax5seglem4  29026  ax5seglem5  29027  axcontlem3  29060  axcontlem8  29065  axcontlem9  29066  eengtrkg  29080  frgr3v  30370  xrofsup  32866  lmhmimasvsca  33125  erdszelem8  35433  resconn  35481  cvmliftmolem2  35517  cvmlift2lem12  35549  r1peuqusdeg1  35878  broutsideof3  36361  outsideoftr  36364  outsidele  36367  ltltncvr  39922  atcvrj2b  39931  cvrat4  39942  cvrat42  39943  2at0mat0  40024  islpln2a  40047  paddasslem11  40329  pmod1i  40347  lhpm0atN  40528  lautcvr  40591  cdlemg4c  41111  tendoplass  41282  tendodi1  41283  tendodi2  41284  dgrsub2  43587  grumnud  44737  ssinc  45541  ssdec  45542  ioondisj2  45945  ioondisj1  45946  ply1mulgsumlem2  48885  catprs  49508  fthcomf  49654  oppcthinco  49936  oppcthinendcALT  49938