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  6112  frfi  9239  wemappo  9509  ttrclss  9680  ttrclselem2  9686  iccsplit  13453  ccatswrd  14640  pfxccat3  14706  modfsummods  15766  pcdvdstr  16854  vdwlem12  16970  cshwsidrepswmod0  17072  iscatd2  17649  oppccomfpropd  17695  initoeu2lem0  17982  resssetc  18061  resscatc  18078  yonedalem4c  18245  mod1ile  18459  mod2ile  18460  prdssgrpd  18667  prdsmndd  18704  grprcan  18912  mulgnn0dir  19043  mulgdir  19045  mulgass  19050  mulgnn0di  19762  mulgdi  19763  dprd2da  19981  lmodprop2d  20837  lssintcl  20877  prdslmodd  20882  islmhm2  20952  islbs2  21071  islbs3  21072  dmatmul  22391  mdetmul  22517  restopnb  23069  iunconn  23322  1stcelcls  23355  blsscls2  24399  stdbdbl  24412  xrsblre  24707  icccmplem2  24719  itg1val2  25592  cvxcl  26902  conway  27718  sleadd1  27903  addsass  27919  mulscom  28049  colline  28583  tglowdim2ln  28585  f1otrg  28805  f1otrge  28806  ax5seglem4  28866  ax5seglem5  28867  axcontlem3  28900  axcontlem8  28905  axcontlem9  28906  eengtrkg  28920  frgr3v  30211  xrofsup  32697  lmhmimasvsca  32987  submomnd  33031  ogrpaddltbi  33039  erdszelem8  35192  resconn  35240  cvmliftmolem2  35276  cvmlift2lem12  35308  r1peuqusdeg1  35637  broutsideof3  36121  outsideoftr  36124  outsidele  36127  ltltncvr  39424  atcvrj2b  39433  cvrat4  39444  cvrat42  39445  2at0mat0  39526  islpln2a  39549  paddasslem11  39831  pmod1i  39849  lhpm0atN  40030  lautcvr  40093  cdlemg4c  40613  tendoplass  40784  tendodi1  40785  tendodi2  40786  dgrsub2  43131  grumnud  44282  ssinc  45088  ssdec  45089  ioondisj2  45498  ioondisj1  45499  ply1mulgsumlem2  48380  catprs  49004  fthcomf  49150  oppcthinco  49432  oppcthinendcALT  49434