Theorem simplr2 1212

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soltmin  5991  frfi  8757  wemappo  9007  iccsplit  12865  ccatswrd  14024  pcdvdstr  16206  vdwlem12  16322  iscatd2  16946  oppccomfpropd  16991  resssetc  17346  resscatc  17359  mod1ile  17709  mod2ile  17710  prdsmndd  17938  grprcan  18131  mulgnn0dir  18251  mulgnn0di  18940  mulgdi  18941  lmodprop2d  19690  lssintcl  19730  prdslmodd  19735  islmhm2  19804  islbs3  19921  mdetmul  21226  restopnb  21777  nrmsep  21959  iunconn  22030  ptpjopn  22214  blsscls2  23108  xrsblre  23413  icccmplem2  23425  icccvx  23548  colline  26429  tglowdim2ln  26431  f1otrg  26651  f1otrge  26652  ax5seglem5  26713  axcontlem3  26746  axcontlem4  26747  axcontlem8  26751  eengtrkg  26766  2pthon3v  27716  erclwwlktr  27794  erclwwlkntr  27844  eucrctshift  28016  frgr3v  28048  frgr2wwlkeqm  28104  xrofsup  30486  submomnd  30706  ogrpaddltbi  30714  erdszelem8  32440  cvmliftmolem2  32524  cvmlift2lem12  32556  conway  33259  btwnswapid  33473  btwnsegle  33573  broutsideof3  33582  outsidele  33588  isbasisrelowllem2  34631  cvrletrN  36403  ltltncvr  36553  atcvrj2b  36562  cvrat4  36573  2at0mat0  36655  islpln2a  36678  paddasslem11  36960  pmod1i  36978  lautcvr  37222  cdlemg4c  37742  tendoplass  37913  tendodi1  37914  tendodi2  37915  mendlmod  39786  mendassa  39787  3adantlr3  41291  ssinc  41346  ssdec  41347  ioondisj2  41759  ioondisj1  41760  stoweidlem60  42338  ply1mulgsumlem2  44434  lincresunit3lem2  44528