Theorem simplr2 1223

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  soltmin  6093  frfi  9192  wemappo  9461  iccsplit  13436  ccatswrd  14629  pcdvdstr  16845  vdwlem12  16961  iscatd2  17645  oppccomfpropd  17691  resssetc  18057  resscatc  18074  mod1ile  18457  mod2ile  18458  prdssgrpd  18699  prdsmndd  18736  grprcan  18947  mulgnn0dir  19078  mulgnn0di  19798  mulgdi  19799  submomnd  20105  ogrpaddltbi  20112  lmodprop2d  20921  lssintcl  20961  prdslmodd  20966  islmhm2  21035  islbs3  21155  mdetmul  22613  restopnb  23165  nrmsep  23347  iunconn  23418  ptpjopn  23602  blsscls2  24494  xrsblre  24802  icccmplem2  24814  icccvx  24942  conway  27796  addsass  28022  mulscom  28156  addonbday  28296  colline  28742  tglowdim2ln  28744  f1otrg  28964  f1otrge  28965  ax5seglem5  29027  axcontlem3  29060  axcontlem4  29061  axcontlem8  29065  eengtrkg  29080  2pthon3v  30036  erclwwlktr  30117  erclwwlkntr  30166  eucrctshift  30338  frgr3v  30370  frgr2wwlkeqm  30426  xrofsup  32866  lmhmimasvsca  33125  erdszelem8  35433  cvmliftmolem2  35517  cvmlift2lem12  35549  r1peuqusdeg1  35878  btwnswapid  36252  btwnsegle  36352  broutsideof3  36361  outsidele  36367  isbasisrelowllem2  37725  cvrletrN  39772  ltltncvr  39922  atcvrj2b  39931  cvrat4  39942  2at0mat0  40024  islpln2a  40047  paddasslem11  40329  pmod1i  40347  lautcvr  40591  cdlemg4c  41111  tendoplass  41282  tendodi1  41283  tendodi2  41284  mendlmod  43641  mendassa  43642  3adantlr3  45495  ssinc  45541  ssdec  45542  ioondisj2  45945  ioondisj1  45946  stoweidlem60  46510  ply1mulgsumlem2  48885  lincresunit3lem2  48978  catprs  49508  fthcomf  49654  oppcthinco  49936  oppcthinendcALT  49938