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  6087  frfi  9176  wemappo  9442  iccsplit  13387  ccatswrd  14578  pcdvdstr  16790  vdwlem12  16906  iscatd2  17589  oppccomfpropd  17635  resssetc  18001  resscatc  18018  mod1ile  18401  mod2ile  18402  prdssgrpd  18643  prdsmndd  18680  grprcan  18888  mulgnn0dir  19019  mulgnn0di  19739  mulgdi  19740  submomnd  20046  ogrpaddltbi  20053  lmodprop2d  20859  lssintcl  20899  prdslmodd  20904  islmhm2  20974  islbs3  21094  mdetmul  22539  restopnb  23091  nrmsep  23273  iunconn  23344  ptpjopn  23528  blsscls2  24420  xrsblre  24728  icccmplem2  24740  icccvx  24876  conway  27741  addsass  27949  mulscom  28079  colline  28628  tglowdim2ln  28630  f1otrg  28850  f1otrge  28851  ax5seglem5  28913  axcontlem3  28946  axcontlem4  28947  axcontlem8  28951  eengtrkg  28966  2pthon3v  29923  erclwwlktr  30004  erclwwlkntr  30053  eucrctshift  30225  frgr3v  30257  frgr2wwlkeqm  30313  xrofsup  32754  lmhmimasvsca  33027  erdszelem8  35263  cvmliftmolem2  35347  cvmlift2lem12  35379  r1peuqusdeg1  35708  btwnswapid  36082  btwnsegle  36182  broutsideof3  36191  outsidele  36197  isbasisrelowllem2  37421  cvrletrN  39392  ltltncvr  39542  atcvrj2b  39551  cvrat4  39562  2at0mat0  39644  islpln2a  39667  paddasslem11  39949  pmod1i  39967  lautcvr  40211  cdlemg4c  40731  tendoplass  40902  tendodi1  40903  tendodi2  40904  mendlmod  43306  mendassa  43307  3adantlr3  45161  ssinc  45208  ssdec  45209  ioondisj2  45617  ioondisj1  45618  stoweidlem60  46182  ply1mulgsumlem2  48512  lincresunit3lem2  48605  catprs  49136  fthcomf  49282  oppcthinco  49564  oppcthinendcALT  49566