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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  soltmin  6156  frfi  9321  wemappo  9589  iccsplit  13525  ccatswrd  14706  pcdvdstr  16914  vdwlem12  17030  iscatd2  17724  oppccomfpropd  17770  resssetc  18137  resscatc  18154  mod1ile  18538  mod2ile  18539  prdssgrpd  18746  prdsmndd  18783  grprcan  18991  mulgnn0dir  19122  mulgnn0di  19843  mulgdi  19844  lmodprop2d  20922  lssintcl  20962  prdslmodd  20967  islmhm2  21037  islbs3  21157  mdetmul  22629  restopnb  23183  nrmsep  23365  iunconn  23436  ptpjopn  23620  blsscls2  24517  xrsblre  24833  icccmplem2  24845  icccvx  24981  conway  27844  addsass  28038  mulscom  28165  colline  28657  tglowdim2ln  28659  f1otrg  28879  f1otrge  28880  ax5seglem5  28948  axcontlem3  28981  axcontlem4  28982  axcontlem8  28986  eengtrkg  29001  2pthon3v  29963  erclwwlktr  30041  erclwwlkntr  30090  eucrctshift  30262  frgr3v  30294  frgr2wwlkeqm  30350  xrofsup  32771  lmhmimasvsca  33044  submomnd  33087  ogrpaddltbi  33095  erdszelem8  35203  cvmliftmolem2  35287  cvmlift2lem12  35319  r1peuqusdeg1  35648  btwnswapid  36018  btwnsegle  36118  broutsideof3  36127  outsidele  36133  isbasisrelowllem2  37357  cvrletrN  39274  ltltncvr  39425  atcvrj2b  39434  cvrat4  39445  2at0mat0  39527  islpln2a  39550  paddasslem11  39832  pmod1i  39850  lautcvr  40094  cdlemg4c  40614  tendoplass  40785  tendodi1  40786  tendodi2  40787  mendlmod  43201  mendassa  43202  3adantlr3  45045  ssinc  45092  ssdec  45093  ioondisj2  45506  ioondisj1  45507  stoweidlem60  46075  ply1mulgsumlem2  48304  lincresunit3lem2  48397  catprs  48900  oppcthinco  49088  oppcthinendcALT  49090