MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-4r Structured version   Visualization version   GIF version

Theorem simp-4r 802
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-4r (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r
StepHypRef Expression
1 simpllr 794 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
21adantr 479 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  simp-5r  804  tfrlem1  7336  injresinj  12406  reuccats1  13278  prdsval  15884  catcocl  16115  catass  16116  catpropd  16138  cidpropd  16139  monpropd  16166  subccocl  16274  funcco  16300  funcpropd  16329  fucpropd  16406  initoeu2lem1  16433  xpcpropd  16617  curf2ndf  16656  drsdirfi  16707  mhmmnd  17306  gsmsymgreqlem2  17620  dfod2  17750  ghmcmn  18006  psgndif  19712  dmatscmcl  20070  smatvscl  20091  cpmatmcllem  20284  pm2mpmhmlem2  20385  chfacfscmulgsum  20426  chfacfpmmulgsum  20430  neitr  20736  1stcrest  21008  dissnref  21083  dissnlocfin  21084  neitx  21162  tgqtop  21267  ptcmplem3  21610  trust  21785  utoptop  21790  restutopopn  21794  ustuqtop2  21798  ustuqtop4  21800  utop3cls  21807  isucn2  21835  met1stc  22077  prdsxmslem2  22085  metustexhalf  22112  cfilucfil  22115  metucn  22127  aannenlem1  23804  ulmuni  23867  lgamucov  24481  pntpbnd  24994  pntlem3  25015  istrkgb  25071  tgbtwndiff  25118  tgifscgr  25121  iscgrglt  25127  tgbtwnconn1lem3  25187  tgbtwnconn1  25188  legov  25198  legtrd  25202  legtri3  25203  ltgseg  25209  legso  25212  tglinethru  25249  tglnpt2  25254  colline  25262  miriso  25283  midexlem  25305  perpneq  25327  isperp2  25328  footex  25331  midex  25347  opphllem3  25359  opphl  25364  hlpasch  25366  lnopp2hpgb  25373  lmieu  25394  trgcopyeu  25416  dfcgra2  25439  f1otrg  25469  axcontlem2  25563  pthdepisspth  25870  usgra2adedgwlkonALT  25910  clwlkfclwwlk  26137  2sqmo  28786  ressprs  28792  omndmul2  28849  isarchi3  28878  isarchiofld  28954  fimaproj  29034  txomap  29035  qtophaus  29037  pstmxmet  29074  sqsscirc1  29088  lmxrge0  29132  esumcst  29258  esumfsup  29265  esum2dlem  29287  esum2d  29288  esumiun  29289  ldsysgenld  29356  sigapildsys  29358  omssubadd  29495  signstfvneq0  29781  afsval  29808  nn0prpwlem  31293  lindsenlbs  32370  matunitlindflem1  32371  matunitlindflem2  32372  mblfinlem3  32414  itg2addnclem  32427  sstotbnd2  32539  prdstotbnd  32559  lcfl8  35605  diophren  36191  rencldnfilem  36198  pellex  36213  pell1234qrdich  36239  pell1qrgap  36252  pellfundex  36264  iunconlem2  37989  suplesup  38293  infleinflem2  38325  xrralrecnnle  38340  limcrecl  38493  limcleqr  38508  0ellimcdiv  38513  limclner  38515  icccncfext  38570  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  fourierdlem50  38846  fourierdlem51  38847  fourierdlem80  38876  fourierdlem87  38883  fourierdlem103  38899  fourierdlem104  38900  omef  39183  smflimlem2  39455  smflimlem4  39457  smfmullem3  39475  reuccatpfxs1  40095  2pthon3v-av  41145  clwlksfclwwlk  41264
  Copyright terms: Public domain W3C validator