Theorem simplr2 1235

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soltmin  6130  frfi  9256  wemappo  9522  iccsplit  13539  ccatswrd  14739  pcdvdstr  16969  vdwlem12  17085  iscatd2  17770  oppccomfpropd  17816  resssetc  18182  resscatc  18199  mod1ile  18582  mod2ile  18583  prdssgrpd  18836  prdsmndd  18878  grprcan  19098  mulgnn0dir  19228  mulgnn0di  19953  mulgdi  19954  submomnd  20260  ogrpaddltbi  20267  lmodprop2d  21109  lssintcl  21149  prdslmodd  21154  islmhm2  21223  islbs3  21343  mdetmul  22846  restopnb  23401  nrmsep  23583  iunconn  23654  ptpjopn  23839  blsscls2  24731  xrsblre  25039  icccmplem2  25051  icccvx  25179  conway  28045  addsass  28271  mulscom  28405  addonbday  28545  colline  28998  tglowdim2ln  29000  f1otrg  29328  f1otrge  29329  ax5seglem5  29391  axcontlem3  29424  axcontlem4  29425  axcontlem8  29429  eengtrkg  29444  2pthon3v  30412  erclwwlktr  30493  erclwwlkntr  30542  eucrctshift  30724  frgr3v  30756  frgr2wwlkeqm  30812  xrofsup  33239  lmhmimasvsca  33479  erdszelem8  35778  cvmliftmolem2  35862  cvmlift2lem12  35894  r1peuqusdeg1  36223  btwnswapid  36598  btwnsegle  36698  broutsideof3  36707  outsidele  36713  nmulprop  36771  nmulcom  36775  isbasisrelowllem2  38111  cvrletrN  40147  ltltncvr  40297  atcvrj2b  40306  cvrat4  40317  2at0mat0  40399  islpln2a  40422  paddasslem11  40704  pmod1i  40722  lautcvr  40966  cdlemg4c  41486  tendoplass  41657  tendodi1  41658  tendodi2  41659  mendlmod  44031  mendassa  44032  3adantlr3  45875  ssinc  45920  ssdec  45921  ioondisj2  46324  ioondisj1  46325  stoweidlem60  46889  ply1mulgsumlem2  49318  lincresunit3lem2  49411  catprs  49938  fthcomf  50084  oppcthinco  50366  oppcthinendcALT  50368