MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1r Structured version   Unicode version

Theorem simp1r 1019
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1r  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 459 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 1015 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  simpl1r  1046  simpr1r  1052  simp11r  1106  simp21r  1112  simp31r  1118  vtoclgft  3154  funprg  5619  omeulem2  7224  uniinqs  7383  unxpdomlem3  7719  elfiun  7882  cofsmo  8640  isfin2-2  8690  isf32lem9  8732  tskun  9153  tskurn  9156  reclem3pr  9416  dedekind  9733  dmdcan  10250  lt2msq1  10423  supmullem1  10504  supmul  10506  xaddass2  11445  xlt2add  11455  xmulasslem3  11481  iccsplit  11656  expaddzlem  12191  expaddz  12192  expmulz  12194  limsupgle  13382  o1add  13518  o1mul  13519  o1sub  13520  bitsfzo  14169  sadfval  14186  smufval  14211  prmexpb  14342  4sqlem18  14564  vdwlem10  14592  mrieqv2d  15128  curf1  15693  mndodcong  16765  subgabl  17043  gex2abl  17056  cntzsubr  17656  abvres  17683  lbsind2  17922  lbsextlem2  18000  lbsextg  18003  matring  19112  mdetunilem8  19288  maducoeval  19308  maducoeval2  19309  madurid  19313  cramerimplem3  19354  pmatcollpw2  19446  pm2mpf1  19467  cnprest  19957  isreg2  20045  fbssfi  20504  hausflimlem  20646  tmdgsum  20760  ssblps  21091  ssbl  21092  xrsmopn  21483  dvres2  22482  vieta1  22874  aalioulem4  22897  efgh  23094  cxpadd  23228  cxpsub  23231  divcxp  23236  cxple2  23246  cxplt2  23247  cxpcn3lem  23289  angcan  23333  ang180lem5  23344  isosctrlem3  23351  brbtwn2  24410  axcontlem4  24472  axcontlem8  24476  clwwlknimp  24978  chscllem4  26756  ogrpinvlt  27948  pstmval  28109  measinblem  28428  cvmlift2lem6  29017  poseq  29573  linethru  30031  cnres2  30499  pellfundex  31061  congtr  31142  fzmaxdif  31158  isnumbasgrplem2  31294  idomsubgmo  31396  upbdrech  31744  mullimc  31861  islptre  31864  mullimcf  31868  neglimc  31892  icccncfext  31929  dvmptfprod  31981  stoweidlem31  32052  domnmsuppn0  33216  mndpfsupp  33223  lincext3  33311  lcv1  35163  lfl1  35192  lshpkrex  35240  hlrelat3  35533  cvrval3  35534  cvrval4N  35535  athgt  35577  atcvrlln2  35640  atcvrlln  35641  lvolnle3at  35703  lvolnlelpln  35706  4atlem11  35730  4atlem12  35733  2lplnj  35741  dalemddea  35805  cdlema2N  35913  paddasslem2  35942  atmod1i1m  35979  lhp2lt  36122  lhp0lt  36124  lhpexle3lem  36132  lhpj1  36143  lhpmcvr4N  36147  lhpelim  36158  lhpmod2i2  36159  lhpmod6i1  36160  cdlemb2  36162  lhpat  36164  ltrnatb  36258  ltrnel  36260  ltrncnvel  36263  ltrncnv  36267  ltrnmwOLD  36273  trlval2  36285  trljat1  36288  trljat2  36289  trlnidatb  36299  cdlemc1  36313  cdlemc2  36314  cdlemc5  36317  cdlemc6  36318  cdleme0aa  36332  cdleme0b  36334  cdleme0c  36335  cdleme0e  36339  cdleme0fN  36340  cdleme01N  36343  cdleme0ex1N  36345  cdleme0moN  36347  cdleme3g  36356  cdleme3h  36357  cdleme3  36359  cdleme4  36360  cdleme4a  36361  cdleme5  36362  cdleme8  36372  cdleme9  36375  cdleme10  36376  cdleme16aN  36381  cdleme11fN  36386  cdleme11g  36387  cdleme11k  36390  cdleme13  36394  cdleme17c  36410  cdleme17d1  36411  cdleme18c  36415  cdleme22gb  36416  cdlemeda  36420  cdlemednpq  36421  cdlemednuN  36422  cdleme19c  36428  cdleme20aN  36432  cdleme20bN  36433  cdleme20c  36434  cdleme22aa  36462  cdleme22d  36466  cdleme22e  36467  cdleme27cl  36489  cdleme27a  36490  cdleme30a  36501  cdleme42a  36594  cdleme42c  36595  cdlemg2fv2  36723  cdlemg2m  36727  cdlemg4g  36739  cdlemg4  36740  cdlemg6c  36743  cdlemg7aN  36748  cdlemg9a  36755  cdlemg9b  36756  cdlemg10c  36762  cdlemg12a  36766  cdlemg12b  36767  cdlemg17a  36784  cdlemg18b  36802  cdlemg18c  36803  trlcoabs2N  36845  trlcolem  36849  tendoco2  36891  tendoicl  36919  cdlemi1  36941  cdlemi2  36942  cdlemj3  36946  tendocan  36947  cdlemk3  36956  cdlemk4  36957  cdlemk5a  36958  cdlemk9  36962  cdlemk9bN  36963  cdlemk10  36966  cdlemk30  37017  cdlemk31  37019  cdlemk39  37039  cdlemkfid1N  37044  cdlemkfid2N  37046  cdlemk19ylem  37053  cdlemk19xlem  37065  cdlemk53b  37079  cdlemk53  37080  cdlemk55a  37082  cdlemk43N  37086  cdlemk19u1  37092  cdlemm10N  37242  cdlemn2  37319  cdlemn10  37330  dihjustlem  37340  dihord2cN  37345  dihvalcq2  37371  dihopelvalcpre  37372  dihord5b  37383  dihord6b  37384  dihmeetlem2N  37423  dihmeetbclemN  37428  dihmeetlem4preN  37430  dihmeetALTN  37451  dochshpncl  37508  dochsatshpb  37576  hdmapval3N  37965  hgmap11  38029
  Copyright terms: Public domain W3C validator