Theorem simplr2 1218

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

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

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

This theorem is referenced by:  soltmin  6099  frfi  9195  wemappo  9464  iccsplit  13438  ccatswrd  14631  pcdvdstr  16847  vdwlem12  16963  iscatd2  17647  oppccomfpropd  17693  resssetc  18059  resscatc  18076  mod1ile  18459  mod2ile  18460  prdssgrpd  18701  prdsmndd  18738  grprcan  18949  mulgnn0dir  19080  mulgnn0di  19800  mulgdi  19801  submomnd  20107  ogrpaddltbi  20114  lmodprop2d  20919  lssintcl  20959  prdslmodd  20964  islmhm2  21033  islbs3  21153  mdetmul  22588  restopnb  23140  nrmsep  23322  iunconn  23393  ptpjopn  23577  blsscls2  24469  xrsblre  24777  icccmplem2  24789  icccvx  24917  conway  27771  addsass  27997  mulscom  28131  addonbday  28271  colline  28717  tglowdim2ln  28719  f1otrg  28939  f1otrge  28940  ax5seglem5  29002  axcontlem3  29035  axcontlem4  29036  axcontlem8  29040  eengtrkg  29055  2pthon3v  30011  erclwwlktr  30092  erclwwlkntr  30141  eucrctshift  30313  frgr3v  30345  frgr2wwlkeqm  30401  xrofsup  32840  lmhmimasvsca  33099  erdszelem8  35380  cvmliftmolem2  35464  cvmlift2lem12  35496  r1peuqusdeg1  35825  btwnswapid  36199  btwnsegle  36299  broutsideof3  36308  outsidele  36314  isbasisrelowllem2  37672  cvrletrN  39719  ltltncvr  39869  atcvrj2b  39878  cvrat4  39889  2at0mat0  39971  islpln2a  39994  paddasslem11  40276  pmod1i  40294  lautcvr  40538  cdlemg4c  41058  tendoplass  41229  tendodi1  41230  tendodi2  41231  mendlmod  43617  mendassa  43618  3adantlr3  45471  ssinc  45517  ssdec  45518  ioondisj2  45923  ioondisj1  45924  stoweidlem60  46488  ply1mulgsumlem2  48863  lincresunit3lem2  48956  catprs  49486  fthcomf  49632  oppcthinco  49914  oppcthinendcALT  49916