Theorem simplr2 1233

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simplr2	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

Proof of Theorem simplr2

Step	Hyp	Ref	Expression
1		simp2 1153	. 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  iccsplit  13503  ccatswrd  14696  pcdvdstr  16926  vdwlem12  17042  iscatd2  17727  oppccomfpropd  17773  resssetc  18139  resscatc  18156  mod1ile  18539  mod2ile  18540  prdssgrpd  18781  prdsmndd  18818  grprcan  19030  mulgnn0dir  19161  mulgnn0di  19886  mulgdi  19887  submomnd  20193  ogrpaddltbi  20200  lmodprop2d  21014  lssintcl  21054  prdslmodd  21059  islmhm2  21128  islbs3  21248  mdetmul  22741  restopnb  23293  nrmsep  23475  iunconn  23546  ptpjopn  23730  blsscls2  24622  xrsblre  24930  icccmplem2  24942  icccvx  25070  conway  27930  addsass  28156  mulscom  28290  addonbday  28430  colline  28877  tglowdim2ln  28879  f1otrg  29129  f1otrge  29130  ax5seglem5  29192  axcontlem3  29225  axcontlem4  29226  axcontlem8  29230  eengtrkg  29245  2pthon3v  30201  erclwwlktr  30282  erclwwlkntr  30331  eucrctshift  30503  frgr3v  30535  frgr2wwlkeqm  30591  xrofsup  33024  lmhmimasvsca  33271  erdszelem8  35561  cvmliftmolem2  35645  cvmlift2lem12  35677  r1peuqusdeg1  36006  btwnswapid  36380  btwnsegle  36480  broutsideof3  36489  outsidele  36495  nmulprop  36553  nmulcom  36557  isbasisrelowllem2  37862  cvrletrN  39909  ltltncvr  40059  atcvrj2b  40068  cvrat4  40079  2at0mat0  40161  islpln2a  40184  paddasslem11  40466  pmod1i  40484  lautcvr  40728  cdlemg4c  41248  tendoplass  41419  tendodi1  41420  tendodi2  41421  mendlmod  43778  mendassa  43779  3adantlr3  45618  ssinc  45663  ssdec  45664  ioondisj2  46067  ioondisj1  46068  stoweidlem60  46632  ply1mulgsumlem2  49018  lincresunit3lem2  49111  catprs  49640  fthcomf  49786  oppcthinco  50068  oppcthinendcALT  50070