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  6129  frfi  9279  wemappo  9546  iccsplit  13619  ccatswrd  14822  pcdvdstr  17059  vdwlem12  17175  iscatd2  17860  oppccomfpropd  17906  resssetc  18272  resscatc  18289  mod1ile  18672  mod2ile  18673  prdssgrpd  18927  prdsmndd  18969  grprcan  19189  mulgnn0dir  19319  mulgnn0di  20044  mulgdi  20045  submomnd  20351  ogrpaddltbi  20358  lmodprop2d  21204  lssintcl  21244  prdslmodd  21249  islmhm2  21318  islbs3  21438  mdetmul  22943  restopnb  23498  nrmsep  23680  iunconn  23751  ptpjopn  23936  blsscls2  24828  xrsblre  25136  icccmplem2  25148  icccvx  25276  conway  28170  addsass  28396  mulscom  28530  addonbday  28670  colline  29123  tglowdim2ln  29125  f1otrg  29453  f1otrge  29454  ax5seglem5  29516  axcontlem3  29549  axcontlem4  29550  axcontlem8  29554  eengtrkg  29569  2pthon3v  30537  erclwwlktr  30618  erclwwlkntr  30667  eucrctshift  30849  frgr3v  30881  frgr2wwlkeqm  30937  xrofsup  33405  lmhmimasvsca  33645  erdszelem8  36049  cvmliftmolem2  36133  cvmlift2lem12  36165  r1peuqusdeg1  36494  btwnswapid  36874  btwnsegle  36974  broutsideof3  36983  outsidele  36989  nmulprop  37031  nmulcom  37035  isbasisrelowllem2  38372  cvrletrN  40423  ltltncvr  40573  atcvrj2b  40582  cvrat4  40593  2at0mat0  40675  islpln2a  40698  paddasslem11  40980  pmod1i  40998  lautcvr  41242  cdlemg4c  41762  tendoplass  41933  tendodi1  41934  tendodi2  41935  mendlmod  44284  mendassa  44285  3adantlr3  46150  ssinc  46195  ssdec  46196  ioondisj2  46598  ioondisj1  46599  stoweidlem60  47163  ply1mulgsumlem2  49592  lincresunit3lem2  49685  catprs  50218  fthcomf  50366  oppcthinco  50667  oppcthinendcALT  50669