Theorem simp-4r 784

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 399

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 400

This theorem is referenced by:  fimaproj  7902  tfrlem1  8112  injresinj  13363  swrdccatin1  14290  reuccatpfxs1  14312  prdsval  16960  catcocl  17188  catass  17189  catpropd  17212  cidpropd  17213  monpropd  17242  subccocl  17351  funcco  17377  funcpropd  17407  fucpropd  17486  initoeu2lem1  17520  xpcpropd  17716  curf2ndf  17755  drsdirfi  17812  mhmmnd  18485  gsmsymgreqlem2  18823  dfod2  18955  ghmcmn  19217  psgndif  20564  mhpmulcl  21089  dmatscmcl  21400  smatvscl  21421  cpmatmcllem  21615  pm2mpmhmlem2  21716  chfacfscmulgsum  21757  chfacfpmmulgsum  21761  neitr  22077  1stcrest  22350  dissnref  22425  dissnlocfin  22426  neitx  22504  tgqtop  22609  ptcmplem3  22951  trust  23127  utoptop  23132  restutopopn  23136  ustuqtop2  23140  ustuqtop4  23142  utop3cls  23149  met1stc  23419  prdsxmslem2  23427  metustexhalf  23454  cfilucfil  23457  metucn  23469  aannenlem1  25221  ulmuni  25284  lgamucov  25920  2sqmo  26318  pntpbnd  26469  pntlem3  26490  istrkgb  26546  tgbtwndiff  26597  tgifscgr  26599  iscgrglt  26605  tgbtwnconn1lem3  26665  tgbtwnconn1  26666  legov  26676  legtrd  26680  legtri3  26681  ltgseg  26687  legso  26690  tglinethru  26727  tglnpt2  26732  colline  26740  miriso  26761  midexlem  26783  perpneq  26805  isperp2  26806  footexALT  26809  footex  26812  midex  26828  opphllem3  26840  opphl  26845  hlpasch  26847  lnopp2hpgb  26854  lmieu  26875  trgcopyeu  26897  dfcgra2  26921  f1otrg  26962  axcontlem2  27056  2pthon3v  28027  2ndresdju  30705  fnpreimac  30728  fsumiunle  30863  ressprs  30960  dfmgc2  30993  mgcf1o  31000  omndmul2  31057  tocyccntz  31130  cyc3genpm  31138  cycpmconjs  31142  cyc3conja  31143  isarchi3  31160  isarchiofld  31235  imaslmod  31267  nsgqusf1olem1  31312  nsgqusf1olem3  31314  intlidl  31316  elrspunidl  31320  idlinsubrg  31322  rhmimaidl  31323  isprmidlc  31337  rhmpreimaprmidl  31341  qsidomlem2  31343  mxidlprm  31354  ssmxidllem  31355  ssmxidl  31356  lbsdiflsp0  31421  dimkerim  31422  fedgmul  31426  ist0cld  31497  txomap  31498  qtophaus  31500  zarcls1  31533  zarclsint  31536  zarclssn  31537  pstmxmet  31561  sqsscirc1  31572  lmxrge0  31616  esumcst  31743  esumfsup  31750  esum2dlem  31772  esum2d  31773  esumiun  31774  ldsysgenld  31840  sigapildsys  31842  omssubadd  31979  signstfvneq0  32263  actfunsnf1o  32296  afsval  32363  noetasuplem4  33676  noetainflem4  33680  nn0prpwlem  34248  lindsenlbs  35509  matunitlindflem1  35510  matunitlindflem2  35511  mblfinlem3  35553  itg2addnclem  35565  sstotbnd2  35669  prdstotbnd  35689  lcfl8  39253  dffltz  40174  flt4lem7  40199  nna4b4nsq  40200  diophren  40338  rencldnfilem  40345  pellex  40360  pell1234qrdich  40386  pell1qrgap  40399  pellfundex  40411  iunconnlem2  42228  suplesup  42551  infleinflem2  42583  xrralrecnnle  42595  rexabslelem  42631  limcrecl  42845  limcleqr  42860  0ellimcdiv  42865  limclner  42867  limsupubuz  42929  limsupvaluz2  42954  supcnvlimsup  42956  climxrre  42966  xlimmnfvlem2  43049  xlimmnfv  43050  xlimpnfvlem2  43053  xlimpnfv  43054  icccncfext  43103  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  fourierdlem50  43372  fourierdlem51  43373  fourierdlem80  43402  fourierdlem87  43409  fourierdlem103  43425  fourierdlem104  43426  meaiuninc3v  43697  omef  43709  smflimlem2  43979  smflimlem4  43981  smfmullem3  43999