Theorem simplr2 1213

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  soltmin  5963  frfi  8747  wemappo  8997  iccsplit  12863  ccatswrd  14021  pcdvdstr  16202  vdwlem12  16318  iscatd2  16944  oppccomfpropd  16989  resssetc  17344  resscatc  17357  mod1ile  17707  mod2ile  17708  prdsmndd  17936  grprcan  18129  mulgnn0dir  18249  mulgnn0di  18939  mulgdi  18940  lmodprop2d  19689  lssintcl  19729  prdslmodd  19734  islmhm2  19803  islbs3  19920  mdetmul  21228  restopnb  21780  nrmsep  21962  iunconn  22033  ptpjopn  22217  blsscls2  23111  xrsblre  23416  icccmplem2  23428  icccvx  23555  colline  26443  tglowdim2ln  26445  f1otrg  26665  f1otrge  26666  ax5seglem5  26727  axcontlem3  26760  axcontlem4  26761  axcontlem8  26765  eengtrkg  26780  2pthon3v  27729  erclwwlktr  27807  erclwwlkntr  27856  eucrctshift  28028  frgr3v  28060  frgr2wwlkeqm  28116  xrofsup  30518  submomnd  30761  ogrpaddltbi  30769  erdszelem8  32558  cvmliftmolem2  32642  cvmlift2lem12  32674  conway  33377  btwnswapid  33591  btwnsegle  33691  broutsideof3  33700  outsidele  33706  isbasisrelowllem2  34773  cvrletrN  36569  ltltncvr  36719  atcvrj2b  36728  cvrat4  36739  2at0mat0  36821  islpln2a  36844  paddasslem11  37126  pmod1i  37144  lautcvr  37388  cdlemg4c  37908  tendoplass  38079  tendodi1  38080  tendodi2  38081  mendlmod  40137  mendassa  40138  3adantlr3  41670  ssinc  41723  ssdec  41724  ioondisj2  42130  ioondisj1  42131  stoweidlem60  42702  ply1mulgsumlem2  44795  lincresunit3lem2  44889