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  6093  frfi  9185  wemappo  9454  ttrclss  9629  ttrclselem2  9635  iccsplit  13401  ccatswrd  14592  pfxccat3  14657  modfsummods  15716  pcdvdstr  16804  vdwlem12  16920  cshwsidrepswmod0  17022  iscatd2  17604  oppccomfpropd  17650  initoeu2lem0  17937  resssetc  18016  resscatc  18033  yonedalem4c  18200  mod1ile  18416  mod2ile  18417  prdssgrpd  18658  prdsmndd  18695  grprcan  18903  mulgnn0dir  19034  mulgdir  19036  mulgass  19041  mulgnn0di  19754  mulgdi  19755  dprd2da  19973  submomnd  20061  ogrpaddltbi  20068  lmodprop2d  20875  lssintcl  20915  prdslmodd  20920  islmhm2  20990  islbs2  21109  islbs3  21110  dmatmul  22441  mdetmul  22567  restopnb  23119  iunconn  23372  1stcelcls  23405  blsscls2  24448  stdbdbl  24461  xrsblre  24756  icccmplem2  24768  itg1val2  25641  cvxcl  26951  conway  27775  leadds1  27985  addsass  28001  mulscom  28135  addonbday  28275  colline  28721  tglowdim2ln  28723  f1otrg  28943  f1otrge  28944  ax5seglem4  29005  ax5seglem5  29006  axcontlem3  29039  axcontlem8  29044  axcontlem9  29045  eengtrkg  29059  frgr3v  30350  xrofsup  32847  lmhmimasvsca  33121  erdszelem8  35392  resconn  35440  cvmliftmolem2  35476  cvmlift2lem12  35508  r1peuqusdeg1  35837  broutsideof3  36320  outsideoftr  36323  outsidele  36326  ltltncvr  39679  atcvrj2b  39688  cvrat4  39699  cvrat42  39700  2at0mat0  39781  islpln2a  39804  paddasslem11  40086  pmod1i  40104  lhpm0atN  40285  lautcvr  40348  cdlemg4c  40868  tendoplass  41039  tendodi1  41040  tendodi2  41041  dgrsub2  43373  grumnud  44523  ssinc  45327  ssdec  45328  ioondisj2  45735  ioondisj1  45736  ply1mulgsumlem2  48629  catprs  49252  fthcomf  49398  oppcthinco  49680  oppcthinendcALT  49682