Theorem simplr2 1229

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  soltmin  6120  frfi  9225  wemappo  9494  iccsplit  13486  ccatswrd  14679  pcdvdstr  16895  vdwlem12  17011  iscatd2  17696  oppccomfpropd  17742  resssetc  18108  resscatc  18125  mod1ile  18508  mod2ile  18509  prdssgrpd  18750  prdsmndd  18787  grprcan  18998  mulgnn0dir  19129  mulgnn0di  19848  mulgdi  19849  submomnd  20155  ogrpaddltbi  20162  lmodprop2d  20971  lssintcl  21011  prdslmodd  21016  islmhm2  21085  islbs3  21205  mdetmul  22663  restopnb  23215  nrmsep  23397  iunconn  23468  ptpjopn  23652  blsscls2  24544  xrsblre  24852  icccmplem2  24864  icccvx  24992  conway  27849  addsass  28075  mulscom  28209  addonbday  28349  colline  28795  tglowdim2ln  28797  f1otrg  29017  f1otrge  29018  ax5seglem5  29080  axcontlem3  29113  axcontlem4  29114  axcontlem8  29118  eengtrkg  29133  2pthon3v  30089  erclwwlktr  30170  erclwwlkntr  30219  eucrctshift  30391  frgr3v  30423  frgr2wwlkeqm  30479  xrofsup  32919  lmhmimasvsca  33178  erdszelem8  35512  cvmliftmolem2  35596  cvmlift2lem12  35628  r1peuqusdeg1  35957  btwnswapid  36331  btwnsegle  36431  broutsideof3  36440  outsidele  36446  nmulprop  36504  nmulcom  36508  isbasisrelowllem2  37814  cvrletrN  39861  ltltncvr  40011  atcvrj2b  40020  cvrat4  40031  2at0mat0  40113  islpln2a  40136  paddasslem11  40418  pmod1i  40436  lautcvr  40680  cdlemg4c  41200  tendoplass  41371  tendodi1  41372  tendodi2  41373  mendlmod  43730  mendassa  43731  3adantlr3  45584  ssinc  45629  ssdec  45630  ioondisj2  46033  ioondisj1  46034  stoweidlem60  46598  ply1mulgsumlem2  48973  lincresunit3lem2  49066  catprs  49596  fthcomf  49742  oppcthinco  50024  oppcthinendcALT  50026