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 739	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  soltmin  6138  frfi  9246  wemappo  9512  iccsplit  13513  ccatswrd  14708  pcdvdstr  16937  vdwlem12  17053  iscatd2  17738  oppccomfpropd  17784  resssetc  18150  resscatc  18167  mod1ile  18550  mod2ile  18551  prdssgrpd  18792  prdsmndd  18829  grprcan  19041  mulgnn0dir  19171  mulgnn0di  19896  mulgdi  19897  submomnd  20203  ogrpaddltbi  20210  lmodprop2d  21026  lssintcl  21066  prdslmodd  21071  islmhm2  21140  islbs3  21260  mdetmul  22761  restopnb  23313  nrmsep  23495  iunconn  23566  ptpjopn  23750  blsscls2  24642  xrsblre  24950  icccmplem2  24962  icccvx  25090  conway  27950  addsass  28176  mulscom  28310  addonbday  28450  colline  28901  tglowdim2ln  28903  f1otrg  29198  f1otrge  29199  ax5seglem5  29261  axcontlem3  29294  axcontlem4  29295  axcontlem8  29299  eengtrkg  29314  2pthon3v  30270  erclwwlktr  30351  erclwwlkntr  30400  eucrctshift  30572  frgr3v  30604  frgr2wwlkeqm  30660  xrofsup  33090  lmhmimasvsca  33336  erdszelem8  35668  cvmliftmolem2  35752  cvmlift2lem12  35784  r1peuqusdeg1  36113  btwnswapid  36487  btwnsegle  36587  broutsideof3  36596  outsidele  36602  nmulprop  36660  nmulcom  36664  isbasisrelowllem2  37980  cvrletrN  40025  ltltncvr  40175  atcvrj2b  40184  cvrat4  40195  2at0mat0  40277  islpln2a  40300  paddasslem11  40582  pmod1i  40600  lautcvr  40844  cdlemg4c  41364  tendoplass  41535  tendodi1  41536  tendodi2  41537  mendlmod  43896  mendassa  43897  3adantlr3  45740  ssinc  45785  ssdec  45786  ioondisj2  46189  ioondisj1  46190  stoweidlem60  46754  ply1mulgsumlem2  49144  lincresunit3lem2  49237  catprs  49766  fthcomf  49912  oppcthinco  50194  oppcthinendcALT  50196