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  6083  frfi  9169  wemappo  9435  iccsplit  13382  ccatswrd  14573  pcdvdstr  16785  vdwlem12  16901  iscatd2  17584  oppccomfpropd  17630  resssetc  17996  resscatc  18013  mod1ile  18396  mod2ile  18397  prdssgrpd  18638  prdsmndd  18675  grprcan  18883  mulgnn0dir  19014  mulgnn0di  19735  mulgdi  19736  submomnd  20042  ogrpaddltbi  20049  lmodprop2d  20855  lssintcl  20895  prdslmodd  20900  islmhm2  20970  islbs3  21090  mdetmul  22536  restopnb  23088  nrmsep  23270  iunconn  23341  ptpjopn  23525  blsscls2  24417  xrsblre  24725  icccmplem2  24737  icccvx  24873  conway  27738  addsass  27946  mulscom  28076  colline  28625  tglowdim2ln  28627  f1otrg  28847  f1otrge  28848  ax5seglem5  28909  axcontlem3  28942  axcontlem4  28943  axcontlem8  28947  eengtrkg  28962  2pthon3v  29919  erclwwlktr  29997  erclwwlkntr  30046  eucrctshift  30218  frgr3v  30250  frgr2wwlkeqm  30306  xrofsup  32745  lmhmimasvsca  33015  erdszelem8  35230  cvmliftmolem2  35314  cvmlift2lem12  35346  r1peuqusdeg1  35675  btwnswapid  36050  btwnsegle  36150  broutsideof3  36159  outsidele  36165  isbasisrelowllem2  37389  cvrletrN  39311  ltltncvr  39461  atcvrj2b  39470  cvrat4  39481  2at0mat0  39563  islpln2a  39586  paddasslem11  39868  pmod1i  39886  lautcvr  40130  cdlemg4c  40650  tendoplass  40821  tendodi1  40822  tendodi2  40823  mendlmod  43221  mendassa  43222  3adantlr3  45076  ssinc  45123  ssdec  45124  ioondisj2  45532  ioondisj1  45533  stoweidlem60  46097  ply1mulgsumlem2  48418  lincresunit3lem2  48511  catprs  49042  fthcomf  49188  oppcthinco  49470  oppcthinendcALT  49472