Theorem simp-4r 795

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 745	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fimaproj  8132  tfrlem1  8363  injresinj  13822  swrdccatin1  14764  reuccatpfxs1  14786  prdsval  17509  catcocl  17742  catass  17743  catpropd  17766  cidpropd  17767  monpropd  17795  subccocl  17903  funcco  17929  funcpropd  17960  fucpropd  18038  initoeu2lem1  18072  xpcpropd  18265  curf2ndf  18304  drsdirfi  18362  chnind  18678  chnub  18679  chnso  18681  mhmmnd  19131  ghmqusnsg  19353  ghmquskerlem3  19357  gsmsymgreqlem2  19502  dfod2  19635  ghmcmn  19902  omndmul2  20204  isdrng4  20826  drngidl  21366  rhmqusnsg  21406  isprmidlc  21453  rhmpreimaprmidl  21460  qsidomlem2  21462  ssdifidllem  21465  ssdifidlprm  21467  psgndif  21733  dmatscmcl  22641  smatvscl  22662  cpmatmcllem  22856  pm2mpmhmlem2  22957  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  neitr  23318  1stcrest  23591  dissnref  23666  dissnlocfin  23667  neitx  23745  tgqtop  23850  ptcmplem3  24192  trust  24367  utoptop  24372  restutopopn  24376  ustuqtop2  24380  ustuqtop4  24382  utop3cls  24389  met1stc  24659  prdsxmslem2  24667  metustexhalf  24694  cfilucfil  24697  metucn  24709  aannenlem1  26470  ulmuni  26533  lgamucov  27180  2sqmo  27579  pntpbnd  27730  pntlem3  27751  noetasuplem4  27878  noetainflem4  27882  bdayfinbndlem1  28638  tgbtwndiff  28753  tgifscgr  28755  iscgrglt  28761  tgbtwnconn1lem3  28821  tgbtwnconn1  28822  legov  28832  legtrd  28836  legtri3  28837  ltgseg  28843  legso  28846  tglinethru  28887  tglinesseq  28891  colline  28901  tglnpt2  28904  tglnpt4  28906  miriso  28925  midexlem  28947  perpneq  28972  isperp2  28973  footexALT  28976  footex  28979  midex  28996  opphllem3  29008  opphl  29013  hlpasch  29016  lnopp2hpgb  29023  plngcplem  29045  lnssplng  29052  plng3p  29057  lmieu  29071  trgcopyeu  29095  dfcgra2  29119  ragcgra  29124  cgrarag  29125  ragsupplcgra  29126  prlnghpg  29174  dfprlng2  29175  dfprlng3  29176  perpprlng  29178  prlngex  29179  prlngmolem1  29180  prlngmolem2  29181  quadcgrprlng  29194  f1otrg  29198  axcontlem2  29293  2pthon3v  30270  2ndresdju  32972  fnpreimac  32993  fsumiunle  33151  ressprs  33264  dfmgc2  33294  mgcf1o  33301  mndlrinvb  33323  mndlactf1o  33328  gsumfs2d  33359  gsumwun  33374  gsumwrd2dccatlem  33375  tocyccntz  33442  cyc3genpm  33450  cycpmconjs  33454  cyc3conja  33455  isarchi3  33485  isarchiofld  33497  elrgspnlem4  33543  erler  33563  elrlocbasi  33565  rlocaddval  33567  rlocmulval  33568  rloccring  33569  rlocf1  33572  rlocisunit  33574  ricdomn1  33587  fracfld  33607  imaslmod  33651  dvdsruasso  33676  nsgqusf1olem1  33700  nsgqusf1olem3  33702  lmhmqusker  33704  intlidl  33706  rhmquskerlem  33711  elrspunidl  33714  elrspunsn  33715  idlinsubrg  33717  rhmimaidl  33718  mxidlprm  33731  mxidlirredi  33732  ssmxidllem  33734  ssmxidl  33735  opprqusplusg  33749  opprqusmulr  33751  qsdrngi  33755  qsdrng  33757  drnglring  33760  dflring2  33761  dflringlem3  33764  dflring4  33766  rsprprmprmidlb  33791  rprmdvdsprod  33802  1arithidom  33805  1arithufdlem2  33813  1arithufdlem3  33814  dfufd2lem  33817  r1plmhm  33877  r1pquslmic  33878  mplidomlem  33895  lbsdiflsp0  33994  dimkerim  33995  fedgmul  33999  fldextrspunlsplem  34041  extdgfialg  34062  constrconj  34113  constrfin  34114  constrelextdg2  34115  constrextdg2lem  34116  constrfiss  34119  ist0cld  34201  txomap  34202  qtophaus  34204  zarcls1  34237  zarclsint  34240  zarclssn  34241  pstmxmet  34265  sqsscirc1  34276  lmxrge0  34320  esumcst  34431  esumfsup  34438  esum2dlem  34460  esum2d  34461  esumiun  34462  ldsysgenld  34528  sigapildsys  34530  omssubadd  34668  signstfvneq0  34937  actfunsnf1o  34969  afsval  35039  nn0prpwlem  36811  lindsenlbs  38244  matunitlindflem1  38245  matunitlindflem2  38246  mblfinlem3  38288  itg2addnclem  38300  sstotbnd2  38403  prdstotbnd  38423  lcfl8  42254  fldhmf1  42835  mndmolinv  42840  primrootscoprmpow  42844  primrootspoweq0  42851  aks6d1c2p2  42864  aks6d1c2lem4  42872  aks6d1c2  42875  aks6d1c5  42884  aks6d1c6lem3  42917  unitscyglem3  42942  fiabv  43284  dffltz  43346  flt4lem7  43371  nna4b4nsq  43372  diophren  43520  rencldnfilem  43527  pellex  43542  pell1234qrdich  43568  pell1qrgap  43581  pellfundex  43593  omabs2  44039  iunconnlem2  45623  modelaxrep  45670  suplesup  46035  infleinflem2  46066  xrralrecnnle  46078  rexabslelem  46112  limcrecl  46325  limcleqr  46338  0ellimcdiv  46343  limclner  46345  limsupubuz  46407  limsupvaluz2  46432  supcnvlimsup  46434  climxrre  46444  xlimmnfvlem2  46527  xlimmnfv  46528  xlimpnfvlem2  46531  xlimpnfv  46532  icccncfext  46581  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  fourierdlem50  46850  fourierdlem51  46851  fourierdlem80  46880  fourierdlem87  46887  fourierdlem103  46903  fourierdlem104  46904  meaiuninc3v  47178  omef  47190  smflimlem2  47466  smflimlem4  47468  smfmullem3  47487  fsupdm  47536  finfdm  47540  chnerlem1  47578  imaf1co  49910  upfval  49931  fuco21  50091  prcofvalg  50131