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  6112  frfi  9239  wemappo  9509  iccsplit  13453  ccatswrd  14640  pcdvdstr  16854  vdwlem12  16970  iscatd2  17649  oppccomfpropd  17695  resssetc  18061  resscatc  18078  mod1ile  18459  mod2ile  18460  prdssgrpd  18667  prdsmndd  18704  grprcan  18912  mulgnn0dir  19043  mulgnn0di  19762  mulgdi  19763  lmodprop2d  20837  lssintcl  20877  prdslmodd  20882  islmhm2  20952  islbs3  21072  mdetmul  22517  restopnb  23069  nrmsep  23251  iunconn  23322  ptpjopn  23506  blsscls2  24399  xrsblre  24707  icccmplem2  24719  icccvx  24855  conway  27718  addsass  27919  mulscom  28049  colline  28583  tglowdim2ln  28585  f1otrg  28805  f1otrge  28806  ax5seglem5  28867  axcontlem3  28900  axcontlem4  28901  axcontlem8  28905  eengtrkg  28920  2pthon3v  29880  erclwwlktr  29958  erclwwlkntr  30007  eucrctshift  30179  frgr3v  30211  frgr2wwlkeqm  30267  xrofsup  32697  lmhmimasvsca  32987  submomnd  33031  ogrpaddltbi  33039  erdszelem8  35192  cvmliftmolem2  35276  cvmlift2lem12  35308  r1peuqusdeg1  35637  btwnswapid  36012  btwnsegle  36112  broutsideof3  36121  outsidele  36127  isbasisrelowllem2  37351  cvrletrN  39273  ltltncvr  39424  atcvrj2b  39433  cvrat4  39444  2at0mat0  39526  islpln2a  39549  paddasslem11  39831  pmod1i  39849  lautcvr  40093  cdlemg4c  40613  tendoplass  40784  tendodi1  40785  tendodi2  40786  mendlmod  43185  mendassa  43186  3adantlr3  45041  ssinc  45088  ssdec  45089  ioondisj2  45498  ioondisj1  45499  stoweidlem60  46065  ply1mulgsumlem2  48380  lincresunit3lem2  48473  catprs  49004  fthcomf  49150  oppcthinco  49432  oppcthinendcALT  49434