Theorem simp-4r 803

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

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

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		simpllr 795	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 480	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simp-5r  805  tfrlem1  7359  injresinj  12451  reuccats1  13332  prdsval  15938  catcocl  16169  catass  16170  catpropd  16192  cidpropd  16193  monpropd  16220  subccocl  16328  funcco  16354  funcpropd  16383  fucpropd  16460  initoeu2lem1  16487  xpcpropd  16671  curf2ndf  16710  drsdirfi  16761  mhmmnd  17360  gsmsymgreqlem2  17674  dfod2  17804  ghmcmn  18060  psgndif  19767  dmatscmcl  20128  smatvscl  20149  cpmatmcllem  20342  pm2mpmhmlem2  20443  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  neitr  20794  1stcrest  21066  dissnref  21141  dissnlocfin  21142  neitx  21220  tgqtop  21325  ptcmplem3  21668  trust  21843  utoptop  21848  restutopopn  21852  ustuqtop2  21856  ustuqtop4  21858  utop3cls  21865  isucn2  21893  met1stc  22136  prdsxmslem2  22144  metustexhalf  22171  cfilucfil  22174  metucn  22186  aannenlem1  23887  ulmuni  23950  lgamucov  24564  pntpbnd  25077  pntlem3  25098  istrkgb  25154  tgbtwndiff  25201  tgifscgr  25203  iscgrglt  25209  tgbtwnconn1lem3  25269  tgbtwnconn1  25270  legov  25280  legtrd  25284  legtri3  25285  ltgseg  25291  legso  25294  tglinethru  25331  tglnpt2  25336  colline  25344  miriso  25365  midexlem  25387  perpneq  25409  isperp2  25410  footex  25413  midex  25429  opphllem3  25441  opphl  25446  hlpasch  25448  lnopp2hpgb  25455  lmieu  25476  trgcopyeu  25498  dfcgra2  25521  f1otrg  25551  axcontlem2  25645  pthdepisspth  26104  usgra2adedgwlkonALT  26144  clwlkfclwwlk  26371  2sqmo  28980  ressprs  28986  omndmul2  29043  isarchi3  29072  isarchiofld  29148  fimaproj  29228  txomap  29229  qtophaus  29231  pstmxmet  29268  sqsscirc1  29282  lmxrge0  29326  esumcst  29452  esumfsup  29459  esum2dlem  29481  esum2d  29482  esumiun  29483  ldsysgenld  29550  sigapildsys  29552  omssubadd  29689  signstfvneq0  29975  afsval  30002  nn0prpwlem  31487  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  mblfinlem3  32618  itg2addnclem  32631  sstotbnd2  32743  prdstotbnd  32763  lcfl8  35809  diophren  36395  rencldnfilem  36402  pellex  36417  pell1234qrdich  36443  pell1qrgap  36456  pellfundex  36468  iunconlem2  38193  suplesup  38496  infleinflem2  38528  xrralrecnnle  38543  limcrecl  38696  limcleqr  38711  0ellimcdiv  38716  limclner  38718  icccncfext  38773  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  fourierdlem50  39049  fourierdlem51  39050  fourierdlem80  39079  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  omef  39386  smflimlem2  39658  smflimlem4  39660  smfmullem3  39678  reuccatpfxs1  40297  2pthon3v-av  41150  clwlksfclwwlk  41269