Theorem simp-4r 783

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 733	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  fimaproj  8075  tfrlem1  8305  injresinj  13709  swrdccatin1  14649  reuccatpfxs1  14671  prdsval  17377  catcocl  17609  catass  17610  catpropd  17633  cidpropd  17634  monpropd  17662  subccocl  17770  funcco  17796  funcpropd  17827  fucpropd  17905  initoeu2lem1  17939  xpcpropd  18132  curf2ndf  18171  drsdirfi  18229  mhmmnd  18961  ghmqusnsg  19179  ghmquskerlem3  19183  gsmsymgreqlem2  19328  dfod2  19461  ghmcmn  19728  omndmul2  20030  rhmqusnsg  21210  psgndif  21527  dmatscmcl  22406  smatvscl  22427  cpmatmcllem  22621  pm2mpmhmlem2  22722  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  neitr  23083  1stcrest  23356  dissnref  23431  dissnlocfin  23432  neitx  23510  tgqtop  23615  ptcmplem3  23957  trust  24133  utoptop  24138  restutopopn  24142  ustuqtop2  24146  ustuqtop4  24148  utop3cls  24155  met1stc  24425  prdsxmslem2  24433  metustexhalf  24460  cfilucfil  24463  metucn  24475  aannenlem1  26252  ulmuni  26317  lgamucov  26964  2sqmo  27364  pntpbnd  27515  pntlem3  27536  noetasuplem4  27664  noetainflem4  27668  tgbtwndiff  28469  tgifscgr  28471  iscgrglt  28477  tgbtwnconn1lem3  28537  tgbtwnconn1  28538  legov  28548  legtrd  28552  legtri3  28553  ltgseg  28559  legso  28562  tglinethru  28599  tglnpt2  28604  colline  28612  miriso  28633  midexlem  28655  perpneq  28677  isperp2  28678  footexALT  28681  footex  28684  midex  28700  opphllem3  28712  opphl  28717  hlpasch  28719  lnopp2hpgb  28726  lmieu  28747  trgcopyeu  28769  dfcgra2  28793  f1otrg  28834  axcontlem2  28928  2pthon3v  29906  2ndresdju  32606  fnpreimac  32628  fsumiunle  32787  ressprs  32921  dfmgc2  32951  mgcf1o  32958  chnind  32966  chnub  32967  chnso  32969  mndlrinvb  32992  mndlactf1o  32997  gsumfs2d  33021  gsumwun  33031  gsumwrd2dccatlem  33032  tocyccntz  33099  cyc3genpm  33107  cycpmconjs  33111  cyc3conja  33112  isarchi3  33139  isarchiofld  33151  elrgspnlem4  33195  erler  33215  elrlocbasi  33216  rlocaddval  33218  rlocmulval  33219  rloccring  33220  rlocf1  33223  isdrng4  33244  fracfld  33257  imaslmod  33300  dvdsruasso  33332  nsgqusf1olem1  33360  nsgqusf1olem3  33362  lmhmqusker  33364  intlidl  33367  rhmquskerlem  33372  elrspunidl  33375  elrspunsn  33376  idlinsubrg  33378  rhmimaidl  33379  drngidl  33380  isprmidlc  33394  rhmpreimaprmidl  33398  qsidomlem2  33400  ssdifidllem  33403  ssdifidlprm  33405  mxidlprm  33417  mxidlirredi  33418  ssmxidllem  33420  ssmxidl  33421  opprqusplusg  33436  opprqusmulr  33438  qsdrngi  33442  qsdrng  33444  rsprprmprmidlb  33470  rprmdvdsprod  33481  1arithidom  33484  1arithufdlem2  33492  1arithufdlem3  33493  dfufd2lem  33496  r1plmhm  33551  r1pquslmic  33552  lbsdiflsp0  33598  dimkerim  33599  fedgmul  33603  fldextrspunlsplem  33644  constrconj  33711  constrfin  33712  constrelextdg2  33713  constrextdg2lem  33714  constrfiss  33717  ist0cld  33799  txomap  33800  qtophaus  33802  zarcls1  33835  zarclsint  33838  zarclssn  33839  pstmxmet  33863  sqsscirc1  33874  lmxrge0  33918  esumcst  34029  esumfsup  34036  esum2dlem  34058  esum2d  34059  esumiun  34060  ldsysgenld  34126  sigapildsys  34128  omssubadd  34267  signstfvneq0  34539  actfunsnf1o  34571  afsval  34638  nn0prpwlem  36295  lindsenlbs  37594  matunitlindflem1  37595  matunitlindflem2  37596  mblfinlem3  37638  itg2addnclem  37650  sstotbnd2  37753  prdstotbnd  37773  lcfl8  41481  fldhmf1  42063  mndmolinv  42068  primrootscoprmpow  42072  primrootspoweq0  42079  aks6d1c2p2  42092  aks6d1c2lem4  42100  aks6d1c2  42103  aks6d1c5  42112  aks6d1c6lem3  42145  unitscyglem3  42170  fiabv  42509  dffltz  42607  flt4lem7  42632  nna4b4nsq  42633  diophren  42786  rencldnfilem  42793  pellex  42808  pell1234qrdich  42834  pell1qrgap  42847  pellfundex  42859  omabs2  43305  iunconnlem2  44908  modelaxrep  44955  suplesup  45319  infleinflem2  45351  xrralrecnnle  45363  rexabslelem  45398  limcrecl  45611  limcleqr  45626  0ellimcdiv  45631  limclner  45633  limsupubuz  45695  limsupvaluz2  45720  supcnvlimsup  45722  climxrre  45732  xlimmnfvlem2  45815  xlimmnfv  45816  xlimpnfvlem2  45819  xlimpnfv  45820  icccncfext  45869  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  fourierdlem50  46138  fourierdlem51  46139  fourierdlem80  46168  fourierdlem87  46175  fourierdlem103  46191  fourierdlem104  46192  meaiuninc3v  46466  omef  46478  smflimlem2  46754  smflimlem4  46756  smfmullem3  46775  fsupdm  46824  finfdm  46828  imaf1co  49141  upfval  49162  fuco21  49322  prcofvalg  49362