Theorem simplr3 1236

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  soltmin  6138  frfi  9246  wemappo  9512  ttrclss  9690  ttrclselem2  9696  iccsplit  13513  ccatswrd  14708  pfxccat3  14773  modfsummods  15847  pcdvdstr  16937  vdwlem12  17053  cshwsidrepswmod0  17155  iscatd2  17738  oppccomfpropd  17784  initoeu2lem0  18071  resssetc  18150  resscatc  18167  yonedalem4c  18334  mod1ile  18550  mod2ile  18551  prdssgrpd  18792  prdsmndd  18829  grprcan  19041  mulgnn0dir  19171  mulgdir  19173  mulgass  19178  mulgnn0di  19896  mulgdi  19897  dprd2da  20115  submomnd  20203  ogrpaddltbi  20210  lmodprop2d  21026  lssintcl  21066  prdslmodd  21071  islmhm2  21140  islbs2  21259  islbs3  21260  dmatmul  22635  mdetmul  22761  restopnb  23313  iunconn  23566  1stcelcls  23599  blsscls2  24642  stdbdbl  24655  xrsblre  24950  icccmplem2  24962  itg1val2  25824  cvxcl  27127  conway  27950  leadds1  28160  addsass  28176  mulscom  28310  addonbday  28450  colline  28901  tglowdim2ln  28903  f1otrg  29198  f1otrge  29199  ax5seglem4  29260  ax5seglem5  29261  axcontlem3  29294  axcontlem8  29299  axcontlem9  29300  eengtrkg  29314  frgr3v  30604  xrofsup  33090  lmhmimasvsca  33336  erdszelem8  35668  resconn  35716  cvmliftmolem2  35752  cvmlift2lem12  35784  r1peuqusdeg1  36113  broutsideof3  36596  outsideoftr  36599  outsidele  36602  nmulprop  36660  nmulcom  36664  ltltncvr  40175  atcvrj2b  40184  cvrat4  40195  cvrat42  40196  2at0mat0  40277  islpln2a  40300  paddasslem11  40582  pmod1i  40600  lhpm0atN  40781  lautcvr  40844  cdlemg4c  41364  tendoplass  41535  tendodi1  41536  tendodi2  41537  dgrsub2  43842  grumnud  44976  ssinc  45785  ssdec  45786  ioondisj2  46189  ioondisj1  46190  ply1mulgsumlem2  49144  catprs  49766  fthcomf  49912  oppcthinco  50194  oppcthinendcALT  50196