Theorem simplr3 1234

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

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

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 1103

This theorem is referenced by:  soltmin  6127  frfi  9233  wemappo  9499  ttrclss  9677  ttrclselem2  9683  iccsplit  13503  ccatswrd  14696  pfxccat3  14761  modfsummods  15835  pcdvdstr  16926  vdwlem12  17042  cshwsidrepswmod0  17144  iscatd2  17727  oppccomfpropd  17773  initoeu2lem0  18060  resssetc  18139  resscatc  18156  yonedalem4c  18323  mod1ile  18539  mod2ile  18540  prdssgrpd  18781  prdsmndd  18818  grprcan  19030  mulgnn0dir  19161  mulgdir  19163  mulgass  19168  mulgnn0di  19886  mulgdi  19887  dprd2da  20105  submomnd  20193  ogrpaddltbi  20200  lmodprop2d  21014  lssintcl  21054  prdslmodd  21059  islmhm2  21128  islbs2  21247  islbs3  21248  dmatmul  22615  mdetmul  22741  restopnb  23293  iunconn  23546  1stcelcls  23579  blsscls2  24622  stdbdbl  24635  xrsblre  24930  icccmplem2  24942  itg1val2  25804  cvxcl  27107  conway  27930  leadds1  28140  addsass  28156  mulscom  28290  addonbday  28430  colline  28877  tglowdim2ln  28879  f1otrg  29129  f1otrge  29130  ax5seglem4  29191  ax5seglem5  29192  axcontlem3  29225  axcontlem8  29230  axcontlem9  29231  eengtrkg  29245  frgr3v  30535  xrofsup  33024  lmhmimasvsca  33271  erdszelem8  35561  resconn  35609  cvmliftmolem2  35645  cvmlift2lem12  35677  r1peuqusdeg1  36006  broutsideof3  36489  outsideoftr  36492  outsidele  36495  nmulprop  36553  nmulcom  36557  ltltncvr  40059  atcvrj2b  40068  cvrat4  40079  cvrat42  40080  2at0mat0  40161  islpln2a  40184  paddasslem11  40466  pmod1i  40484  lhpm0atN  40665  lautcvr  40728  cdlemg4c  41248  tendoplass  41419  tendodi1  41420  tendodi2  41421  dgrsub2  43724  grumnud  44860  ssinc  45663  ssdec  45664  ioondisj2  46067  ioondisj1  46068  ply1mulgsumlem2  49018  catprs  49640  fthcomf  49786  oppcthinco  50068  oppcthinendcALT  50070