Theorem simplr2 1218

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 728	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  6094  frfi  9189  wemappo  9458  iccsplit  13405  ccatswrd  14596  pcdvdstr  16808  vdwlem12  16924  iscatd2  17608  oppccomfpropd  17654  resssetc  18020  resscatc  18037  mod1ile  18420  mod2ile  18421  prdssgrpd  18662  prdsmndd  18699  grprcan  18907  mulgnn0dir  19038  mulgnn0di  19758  mulgdi  19759  submomnd  20065  ogrpaddltbi  20072  lmodprop2d  20879  lssintcl  20919  prdslmodd  20924  islmhm2  20994  islbs3  21114  mdetmul  22571  restopnb  23123  nrmsep  23305  iunconn  23376  ptpjopn  23560  blsscls2  24452  xrsblre  24760  icccmplem2  24772  icccvx  24908  conway  27777  addsass  27987  mulscom  28121  addsonbday  28260  colline  28704  tglowdim2ln  28706  f1otrg  28926  f1otrge  28927  ax5seglem5  28989  axcontlem3  29022  axcontlem4  29023  axcontlem8  29027  eengtrkg  29042  2pthon3v  29999  erclwwlktr  30080  erclwwlkntr  30129  eucrctshift  30301  frgr3v  30333  frgr2wwlkeqm  30389  xrofsup  32828  lmhmimasvsca  33102  erdszelem8  35373  cvmliftmolem2  35457  cvmlift2lem12  35489  r1peuqusdeg1  35818  btwnswapid  36192  btwnsegle  36292  broutsideof3  36301  outsidele  36307  isbasisrelowllem2  37532  cvrletrN  39570  ltltncvr  39720  atcvrj2b  39729  cvrat4  39740  2at0mat0  39822  islpln2a  39845  paddasslem11  40127  pmod1i  40145  lautcvr  40389  cdlemg4c  40909  tendoplass  41080  tendodi1  41081  tendodi2  41082  mendlmod  43467  mendassa  43468  3adantlr3  45321  ssinc  45367  ssdec  45368  ioondisj2  45775  ioondisj1  45776  stoweidlem60  46340  ply1mulgsumlem2  48669  lincresunit3lem2  48762  catprs  49292  fthcomf  49438  oppcthinco  49720  oppcthinendcALT  49722