Theorem simplr2 1217

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

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

This theorem is referenced by:  soltmin  6093  frfi  9185  wemappo  9454  iccsplit  13401  ccatswrd  14592  pcdvdstr  16804  vdwlem12  16920  iscatd2  17604  oppccomfpropd  17650  resssetc  18016  resscatc  18033  mod1ile  18416  mod2ile  18417  prdssgrpd  18658  prdsmndd  18695  grprcan  18903  mulgnn0dir  19034  mulgnn0di  19754  mulgdi  19755  submomnd  20061  ogrpaddltbi  20068  lmodprop2d  20875  lssintcl  20915  prdslmodd  20920  islmhm2  20990  islbs3  21110  mdetmul  22567  restopnb  23119  nrmsep  23301  iunconn  23372  ptpjopn  23556  blsscls2  24448  xrsblre  24756  icccmplem2  24768  icccvx  24904  conway  27775  addsass  28001  mulscom  28135  addonbday  28275  colline  28721  tglowdim2ln  28723  f1otrg  28943  f1otrge  28944  ax5seglem5  29006  axcontlem3  29039  axcontlem4  29040  axcontlem8  29044  eengtrkg  29059  2pthon3v  30016  erclwwlktr  30097  erclwwlkntr  30146  eucrctshift  30318  frgr3v  30350  frgr2wwlkeqm  30406  xrofsup  32847  lmhmimasvsca  33121  erdszelem8  35392  cvmliftmolem2  35476  cvmlift2lem12  35508  r1peuqusdeg1  35837  btwnswapid  36211  btwnsegle  36311  broutsideof3  36320  outsidele  36326  isbasisrelowllem2  37557  cvrletrN  39529  ltltncvr  39679  atcvrj2b  39688  cvrat4  39699  2at0mat0  39781  islpln2a  39804  paddasslem11  40086  pmod1i  40104  lautcvr  40348  cdlemg4c  40868  tendoplass  41039  tendodi1  41040  tendodi2  41041  mendlmod  43427  mendassa  43428  3adantlr3  45281  ssinc  45327  ssdec  45328  ioondisj2  45735  ioondisj1  45736  stoweidlem60  46300  ply1mulgsumlem2  48629  lincresunit3lem2  48722  catprs  49252  fthcomf  49398  oppcthinco  49680  oppcthinendcALT  49682