Theorem simplr2 1216

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 726	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  6168  frfi  9349  wemappo  9618  iccsplit  13545  ccatswrd  14716  pcdvdstr  16923  vdwlem12  17039  iscatd2  17739  oppccomfpropd  17787  resssetc  18159  resscatc  18176  mod1ile  18563  mod2ile  18564  prdssgrpd  18771  prdsmndd  18805  grprcan  19013  mulgnn0dir  19144  mulgnn0di  19867  mulgdi  19868  lmodprop2d  20944  lssintcl  20985  prdslmodd  20990  islmhm2  21060  islbs3  21180  mdetmul  22650  restopnb  23204  nrmsep  23386  iunconn  23457  ptpjopn  23641  blsscls2  24538  xrsblre  24852  icccmplem2  24864  icccvx  25000  conway  27862  addsass  28056  mulscom  28183  colline  28675  tglowdim2ln  28677  f1otrg  28897  f1otrge  28898  ax5seglem5  28966  axcontlem3  28999  axcontlem4  29000  axcontlem8  29004  eengtrkg  29019  2pthon3v  29976  erclwwlktr  30054  erclwwlkntr  30103  eucrctshift  30275  frgr3v  30307  frgr2wwlkeqm  30363  xrofsup  32774  lmhmimasvsca  33025  submomnd  33060  ogrpaddltbi  33068  erdszelem8  35166  cvmliftmolem2  35250  cvmlift2lem12  35282  r1peuqusdeg1  35611  btwnswapid  35981  btwnsegle  36081  broutsideof3  36090  outsidele  36096  isbasisrelowllem2  37322  cvrletrN  39229  ltltncvr  39380  atcvrj2b  39389  cvrat4  39400  2at0mat0  39482  islpln2a  39505  paddasslem11  39787  pmod1i  39805  lautcvr  40049  cdlemg4c  40569  tendoplass  40740  tendodi1  40741  tendodi2  40742  mendlmod  43150  mendassa  43151  3adantlr3  44940  ssinc  44989  ssdec  44990  ioondisj2  45411  ioondisj1  45412  stoweidlem60  45981  ply1mulgsumlem2  48116  lincresunit3lem2  48209  catprs  48678