Theorem simplr2 1214

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  soltmin  6030  frfi  8989  wemappo  9238  iccsplit  13146  ccatswrd  14309  pcdvdstr  16505  vdwlem12  16621  iscatd2  17307  oppccomfpropd  17355  resssetc  17723  resscatc  17740  mod1ile  18126  mod2ile  18127  prdsmndd  18333  grprcan  18528  mulgnn0dir  18648  mulgnn0di  19342  mulgdi  19343  lmodprop2d  20100  lssintcl  20141  prdslmodd  20146  islmhm2  20215  islbs3  20332  mdetmul  21680  restopnb  22234  nrmsep  22416  iunconn  22487  ptpjopn  22671  blsscls2  23566  xrsblre  23880  icccmplem2  23892  icccvx  24019  colline  26914  tglowdim2ln  26916  f1otrg  27136  f1otrge  27137  ax5seglem5  27204  axcontlem3  27237  axcontlem4  27238  axcontlem8  27242  eengtrkg  27257  2pthon3v  28209  erclwwlktr  28287  erclwwlkntr  28336  eucrctshift  28508  frgr3v  28540  frgr2wwlkeqm  28596  xrofsup  30992  submomnd  31238  ogrpaddltbi  31246  erdszelem8  33060  cvmliftmolem2  33144  cvmlift2lem12  33176  conway  33920  btwnswapid  34246  btwnsegle  34346  broutsideof3  34355  outsidele  34361  isbasisrelowllem2  35454  cvrletrN  37214  ltltncvr  37364  atcvrj2b  37373  cvrat4  37384  2at0mat0  37466  islpln2a  37489  paddasslem11  37771  pmod1i  37789  lautcvr  38033  cdlemg4c  38553  tendoplass  38724  tendodi1  38725  tendodi2  38726  mendlmod  40934  mendassa  40935  3adantlr3  42473  ssinc  42526  ssdec  42527  ioondisj2  42921  ioondisj1  42922  stoweidlem60  43491  ply1mulgsumlem2  45616  lincresunit3lem2  45709  catprs  46180