Theorem simp-4r 781

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-4r	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 730	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fimaproj  7985  tfrlem1  8216  injresinj  13517  swrdccatin1  14447  reuccatpfxs1  14469  prdsval  17175  catcocl  17403  catass  17404  catpropd  17427  cidpropd  17428  monpropd  17458  subccocl  17569  funcco  17595  funcpropd  17625  fucpropd  17704  initoeu2lem1  17738  xpcpropd  17935  curf2ndf  17974  drsdirfi  18032  mhmmnd  18706  gsmsymgreqlem2  19048  dfod2  19180  ghmcmn  19442  psgndif  20816  mhpmulcl  21348  dmatscmcl  21661  smatvscl  21682  cpmatmcllem  21876  pm2mpmhmlem2  21977  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  neitr  22340  1stcrest  22613  dissnref  22688  dissnlocfin  22689  neitx  22767  tgqtop  22872  ptcmplem3  23214  trust  23390  utoptop  23395  restutopopn  23399  ustuqtop2  23403  ustuqtop4  23405  utop3cls  23412  met1stc  23686  prdsxmslem2  23694  metustexhalf  23721  cfilucfil  23724  metucn  23736  aannenlem1  25497  ulmuni  25560  lgamucov  26196  2sqmo  26594  pntpbnd  26745  pntlem3  26766  istrkgb  26825  tgbtwndiff  26876  tgifscgr  26878  iscgrglt  26884  tgbtwnconn1lem3  26944  tgbtwnconn1  26945  legov  26955  legtrd  26959  legtri3  26960  ltgseg  26966  legso  26969  tglinethru  27006  tglnpt2  27011  colline  27019  miriso  27040  midexlem  27062  perpneq  27084  isperp2  27085  footexALT  27088  footex  27091  midex  27107  opphllem3  27119  opphl  27124  hlpasch  27126  lnopp2hpgb  27133  lmieu  27154  trgcopyeu  27176  dfcgra2  27200  f1otrg  27241  axcontlem2  27342  2pthon3v  28317  2ndresdju  30995  fnpreimac  31017  fsumiunle  31152  ressprs  31250  dfmgc2  31283  mgcf1o  31290  omndmul2  31347  tocyccntz  31420  cyc3genpm  31428  cycpmconjs  31432  cyc3conja  31433  isarchi3  31450  isarchiofld  31525  imaslmod  31562  nsgqusf1olem1  31607  nsgqusf1olem3  31609  intlidl  31611  elrspunidl  31615  idlinsubrg  31617  rhmimaidl  31618  isprmidlc  31632  rhmpreimaprmidl  31636  qsidomlem2  31638  mxidlprm  31649  ssmxidllem  31650  ssmxidl  31651  lbsdiflsp0  31716  dimkerim  31717  fedgmul  31721  ist0cld  31792  txomap  31793  qtophaus  31795  zarcls1  31828  zarclsint  31831  zarclssn  31832  pstmxmet  31856  sqsscirc1  31867  lmxrge0  31911  esumcst  32040  esumfsup  32047  esum2dlem  32069  esum2d  32070  esumiun  32071  ldsysgenld  32137  sigapildsys  32139  omssubadd  32276  signstfvneq0  32560  actfunsnf1o  32593  afsval  32660  noetasuplem4  33948  noetainflem4  33952  nn0prpwlem  34520  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  mblfinlem3  35825  itg2addnclem  35837  sstotbnd2  35941  prdstotbnd  35961  lcfl8  39523  dffltz  40478  flt4lem7  40503  nna4b4nsq  40504  diophren  40642  rencldnfilem  40649  pellex  40664  pell1234qrdich  40690  pell1qrgap  40703  pellfundex  40715  iunconnlem2  42562  suplesup  42885  infleinflem2  42917  xrralrecnnle  42929  rexabslelem  42965  limcrecl  43177  limcleqr  43192  0ellimcdiv  43197  limclner  43199  limsupubuz  43261  limsupvaluz2  43286  supcnvlimsup  43288  climxrre  43298  xlimmnfvlem2  43381  xlimmnfv  43382  xlimpnfvlem2  43385  xlimpnfv  43386  icccncfext  43435  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  fourierdlem50  43704  fourierdlem51  43705  fourierdlem80  43734  fourierdlem87  43741  fourierdlem103  43757  fourierdlem104  43758  meaiuninc3v  44029  omef  44041  smflimlem2  44317  smflimlem4  44319  smfmullem3  44338