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 824
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 815 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
21adantr 480 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
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 197  df-an 385
This theorem is referenced by:  simp-5r  826  tfrlem1  7517  injresinj  12629  reuccats1  13526  prdsval  16162  catcocl  16393  catass  16394  catpropd  16416  cidpropd  16417  monpropd  16444  subccocl  16552  funcco  16578  funcpropd  16607  fucpropd  16684  initoeu2lem1  16711  xpcpropd  16895  curf2ndf  16934  drsdirfi  16985  mhmmnd  17584  gsmsymgreqlem2  17897  dfod2  18027  ghmcmn  18283  psgndif  19996  dmatscmcl  20357  smatvscl  20378  cpmatmcllem  20571  pm2mpmhmlem2  20672  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  neitr  21032  1stcrest  21304  dissnref  21379  dissnlocfin  21380  neitx  21458  tgqtop  21563  ptcmplem3  21905  trust  22080  utoptop  22085  restutopopn  22089  ustuqtop2  22093  ustuqtop4  22095  utop3cls  22102  isucn2  22130  met1stc  22373  prdsxmslem2  22381  metustexhalf  22408  cfilucfil  22411  metucn  22423  aannenlem1  24128  ulmuni  24191  lgamucov  24809  pntpbnd  25322  pntlem3  25343  istrkgb  25399  tgbtwndiff  25446  tgifscgr  25448  iscgrglt  25454  tgbtwnconn1lem3  25514  tgbtwnconn1  25515  legov  25525  legtrd  25529  legtri3  25530  ltgseg  25536  legso  25539  tglinethru  25576  tglnpt2  25581  colline  25589  miriso  25610  midexlem  25632  perpneq  25654  isperp2  25655  footex  25658  midex  25674  opphllem3  25686  opphl  25691  hlpasch  25693  lnopp2hpgb  25700  lmieu  25721  trgcopyeu  25743  dfcgra2  25766  f1otrg  25796  axcontlem2  25890  2pthon3v  26908  clwlksfclwwlk  27049  fsumiunle  29703  2sqmo  29777  ressprs  29783  omndmul2  29840  isarchi3  29869  isarchiofld  29945  fimaproj  30028  txomap  30029  qtophaus  30031  pstmxmet  30068  sqsscirc1  30082  lmxrge0  30126  esumcst  30253  esumfsup  30260  esum2dlem  30282  esum2d  30283  esumiun  30284  ldsysgenld  30351  sigapildsys  30353  omssubadd  30490  signstfvneq0  30777  actfunsnf1o  30810  afsval  30877  noetalem3  31990  nn0prpwlem  32442  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  mblfinlem3  33578  itg2addnclem  33591  sstotbnd2  33703  prdstotbnd  33723  lcfl8  37108  diophren  37694  rencldnfilem  37701  pellex  37716  pell1234qrdich  37742  pell1qrgap  37755  pellfundex  37767  iunconnlem2  39485  suplesup  39868  infleinflem2  39900  xrralrecnnle  39915  rexabslelem  39958  limcrecl  40179  limcleqr  40194  0ellimcdiv  40199  limclner  40201  limsupubuz  40263  limsupvaluz2  40288  supcnvlimsup  40290  climxrre  40300  xlimmnfvlem2  40377  xlimmnfv  40378  xlimpnfvlem2  40381  xlimpnfv  40382  icccncfext  40418  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  fourierdlem50  40691  fourierdlem51  40692  fourierdlem80  40721  fourierdlem87  40728  fourierdlem103  40744  fourierdlem104  40745  meaiuninc3v  41019  omef  41031  smflimlem2  41301  smflimlem4  41303  smfmullem3  41321  reuccatpfxs1  41759
  Copyright terms: Public domain W3C validator