Theorem simp-4r 780

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 729	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 208  df-an 397

This theorem is referenced by:  tfrlem1  7855  injresinj  12996  reuccatpfxs1  13933  prdsval  16545  catcocl  16773  catass  16774  catpropd  16796  cidpropd  16797  monpropd  16824  subccocl  16932  funcco  16958  funcpropd  16987  fucpropd  17064  initoeu2lem1  17091  xpcpropd  17275  curf2ndf  17314  drsdirfi  17365  mhmmnd  17966  gsmsymgreqlem2  18278  dfod2  18409  ghmcmn  18665  psgndif  20416  dmatscmcl  20784  smatvscl  20805  cpmatmcllem  20998  pm2mpmhmlem2  21099  chfacfscmulgsum  21140  chfacfpmmulgsum  21144  neitr  21460  1stcrest  21733  dissnref  21808  dissnlocfin  21809  neitx  21887  tgqtop  21992  ptcmplem3  22334  trust  22509  utoptop  22514  restutopopn  22518  ustuqtop2  22522  ustuqtop4  22524  utop3cls  22531  met1stc  22802  prdsxmslem2  22810  metustexhalf  22837  cfilucfil  22840  metucn  22852  aannenlem1  24588  ulmuni  24651  lgamucov  25285  2sqmo  25683  pntpbnd  25834  pntlem3  25855  istrkgb  25911  tgbtwndiff  25962  tgifscgr  25964  iscgrglt  25970  tgbtwnconn1lem3  26030  tgbtwnconn1  26031  legov  26041  legtrd  26045  legtri3  26046  ltgseg  26052  legso  26055  tglinethru  26092  tglnpt2  26097  colline  26105  miriso  26126  midexlem  26148  perpneq  26170  isperp2  26171  footexALT  26174  footex  26177  midex  26193  opphllem3  26205  opphl  26210  hlpasch  26212  lnopp2hpgb  26219  lmieu  26240  trgcopyeu  26262  dfcgra2  26286  f1otrg  26328  axcontlem2  26422  2pthon3v  27397  fnpreimac  30079  fsumiunle  30200  ressprs  30286  omndmul2  30343  cyc3genpm  30390  cycpmconjs  30394  cyc3conja  30395  isarchi3  30412  isarchiofld  30499  imaslmod  30531  lbsdiflsp0  30581  dimkerim  30582  fedgmul  30586  fimaproj  30670  txomap  30671  qtophaus  30673  pstmxmet  30710  sqsscirc1  30724  lmxrge0  30768  esumcst  30895  esumfsup  30902  esum2dlem  30924  esum2d  30925  esumiun  30926  ldsysgenld  30992  sigapildsys  30994  omssubadd  31131  signstfvneq0  31415  actfunsnf1o  31448  afsval  31515  noetalem3  32773  nn0prpwlem  33224  lindsenlbs  34364  matunitlindflem1  34365  matunitlindflem2  34366  mblfinlem3  34408  itg2addnclem  34420  sstotbnd2  34530  prdstotbnd  34550  lcfl8  38119  dffltz  38718  diophren  38846  rencldnfilem  38853  pellex  38868  pell1234qrdich  38894  pell1qrgap  38907  pellfundex  38919  iunconnlem2  40760  suplesup  41101  infleinflem2  41133  xrralrecnnle  41148  rexabslelem  41188  limcrecl  41406  limcleqr  41421  0ellimcdiv  41426  limclner  41428  limsupubuz  41490  limsupvaluz2  41515  supcnvlimsup  41517  climxrre  41527  xlimmnfvlem2  41610  xlimmnfv  41611  xlimpnfvlem2  41614  xlimpnfv  41615  icccncfext  41665  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  fourierdlem50  41937  fourierdlem51  41938  fourierdlem80  41967  fourierdlem87  41974  fourierdlem103  41990  fourierdlem104  41991  meaiuninc3v  42262  omef  42274  smflimlem2  42544  smflimlem4  42546  smfmullem3  42564