Theorem simplr2 1215

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  soltmin  6041  frfi  9059  wemappo  9308  iccsplit  13217  ccatswrd  14381  pcdvdstr  16577  vdwlem12  16693  iscatd2  17390  oppccomfpropd  17438  resssetc  17807  resscatc  17824  mod1ile  18211  mod2ile  18212  prdsmndd  18418  grprcan  18613  mulgnn0dir  18733  mulgnn0di  19427  mulgdi  19428  lmodprop2d  20185  lssintcl  20226  prdslmodd  20231  islmhm2  20300  islbs3  20417  mdetmul  21772  restopnb  22326  nrmsep  22508  iunconn  22579  ptpjopn  22763  blsscls2  23660  xrsblre  23974  icccmplem2  23986  icccvx  24113  colline  27010  tglowdim2ln  27012  f1otrg  27232  f1otrge  27233  ax5seglem5  27301  axcontlem3  27334  axcontlem4  27335  axcontlem8  27339  eengtrkg  27354  2pthon3v  28308  erclwwlktr  28386  erclwwlkntr  28435  eucrctshift  28607  frgr3v  28639  frgr2wwlkeqm  28695  xrofsup  31090  submomnd  31336  ogrpaddltbi  31344  erdszelem8  33160  cvmliftmolem2  33244  cvmlift2lem12  33276  conway  33993  btwnswapid  34319  btwnsegle  34419  broutsideof3  34428  outsidele  34434  isbasisrelowllem2  35527  cvrletrN  37287  ltltncvr  37437  atcvrj2b  37446  cvrat4  37457  2at0mat0  37539  islpln2a  37562  paddasslem11  37844  pmod1i  37862  lautcvr  38106  cdlemg4c  38626  tendoplass  38797  tendodi1  38798  tendodi2  38799  mendlmod  41018  mendassa  41019  3adantlr3  42584  ssinc  42637  ssdec  42638  ioondisj2  43031  ioondisj1  43032  stoweidlem60  43601  ply1mulgsumlem2  45728  lincresunit3lem2  45821  catprs  46292