Theorem simplr3 1230

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simplr3	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒)

Proof of Theorem simplr3

Step	Hyp	Ref	Expression
1		simp3 1150	. 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  ttrclss  9672  ttrclselem2  9678  iccsplit  13486  ccatswrd  14679  pfxccat3  14744  modfsummods  15804  pcdvdstr  16895  vdwlem12  17011  cshwsidrepswmod0  17113  iscatd2  17696  oppccomfpropd  17742  initoeu2lem0  18029  resssetc  18108  resscatc  18125  yonedalem4c  18292  mod1ile  18508  mod2ile  18509  prdssgrpd  18750  prdsmndd  18787  grprcan  18998  mulgnn0dir  19129  mulgdir  19131  mulgass  19136  mulgnn0di  19848  mulgdi  19849  dprd2da  20067  submomnd  20155  ogrpaddltbi  20162  lmodprop2d  20971  lssintcl  21011  prdslmodd  21016  islmhm2  21085  islbs2  21204  islbs3  21205  dmatmul  22537  mdetmul  22663  restopnb  23215  iunconn  23468  1stcelcls  23501  blsscls2  24544  stdbdbl  24557  xrsblre  24852  icccmplem2  24864  itg1val2  25726  cvxcl  27026  conway  27849  leadds1  28059  addsass  28075  mulscom  28209  addonbday  28349  colline  28795  tglowdim2ln  28797  f1otrg  29017  f1otrge  29018  ax5seglem4  29079  ax5seglem5  29080  axcontlem3  29113  axcontlem8  29118  axcontlem9  29119  eengtrkg  29133  frgr3v  30423  xrofsup  32919  lmhmimasvsca  33178  erdszelem8  35512  resconn  35560  cvmliftmolem2  35596  cvmlift2lem12  35628  r1peuqusdeg1  35957  broutsideof3  36440  outsideoftr  36443  outsidele  36446  nmulprop  36504  nmulcom  36508  ltltncvr  40011  atcvrj2b  40020  cvrat4  40031  cvrat42  40032  2at0mat0  40113  islpln2a  40136  paddasslem11  40418  pmod1i  40436  lhpm0atN  40617  lautcvr  40680  cdlemg4c  41200  tendoplass  41371  tendodi1  41372  tendodi2  41373  dgrsub2  43676  grumnud  44826  ssinc  45629  ssdec  45630  ioondisj2  46033  ioondisj1  46034  ply1mulgsumlem2  48973  catprs  49596  fthcomf  49742  oppcthinco  50024  oppcthinendcALT  50026