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

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

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 447 . 2  |-  ( ( ch  /\  th )  ->  th )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl3r  1011  simpr3r  1017  simp13r  1071  simp23r  1077  simp33r  1083  disjss3  4038  tfisi  4665  f1oiso2  5865  omeulem1  6596  omeulem2  6597  elfiun  7199  isfin2-2  7961  addid2  9011  mulcan  9421  mulcan2  9422  divass  9458  divdir  9463  div11  9466  ltdiv1  9636  ltmuldiv  9642  lediv2  9662  xaddass2  10586  xlt2add  10596  expaddz  11162  expmulz  11164  resqrex  11752  resqrcl  11755  o1add  12103  o1mul  12104  o1sub  12105  dvdsgcd  12738  rpexp12i  12817  pythagtriplem4  12888  pythagtriplem11  12894  pythagtriplem13  12896  pcpremul  12912  pceu  12915  pcqmul  12922  pcqdiv  12926  f1ocpbllem  13442  funcoppc  13765  funcres  13786  catcisolem  13954  1stfcl  13987  2ndfcl  13988  prfcl  13993  evlfcl  14012  curf1cl  14018  curfcl  14022  hofcl  14049  latjlej12  14189  latmlem12  14205  latj4  14223  latj4rot  14224  odcong  14880  cmn4  15124  ablsub4  15130  abladdsub4  15131  lsm4  15168  abvdom  15619  abvtrivd  15621  lspsolvlem  15911  lbsextlem2  15928  hausflimlem  17690  xmetlecl  17927  prdsxmetlem  17948  xblcntr  17979  bndth  18472  cph2ass  18664  iscau3  18720  dvres2  19278  coemullem  19647  vieta1  19708  aalioulem4  19731  cxpcn3lem  20103  angcan  20116  divsqrsumlem  20290  dchrmusumlema  20658  dchrvmasumlema  20665  dchrisum0lema  20679  logdivsum  20698  padicabv  20795  gxnval  20943  gxnn0mul  20960  adjlnop  22682  xreceu  23121  measvunilem  23555  measvuni  23557  ax5seglem3  24631  ax5seglem6  24634  axpasch  24641  axeuclid  24663  axcontlem4  24667  axcontlem8  24671  cgrcomim  24684  cgrcoml  24691  cgrcomr  24692  cgrdegen  24699  segconeu  24706  btwnintr  24714  btwnexch3  24715  btwnouttr2  24717  btwnouttr  24719  btwnexch  24720  ifscgr  24739  lineext  24771  linecgr  24776  lineid  24778  idinside  24779  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem14  24795  btwnconn2  24797  btwnconn3  24798  midofsegid  24799  btwnoutside  24820  outsideoftr  24824  lineunray  24842  lineelsb2  24843  itg2addnclem  25003  itg2addnc  25005  infxpg  25198  valvalcurfn  25309  prltub  25363  mulinvsca  25583  conttnf2  25665  prdnei  25676  mulmulvec  25790  distsava  25792  cmpmorass  26069  lppotos  26247  cnres2  26586  heibor  26648  mzpmfp  26928  mzpsubst  26929  pellex  27023  pellfundex  27074  pellfund14gap  27075  qirropth  27096  rmxypos  27137  congmul  27157  congsub  27160  mzpcong  27162  coprmdvdsb  27177  jm2.15nn0  27199  jm2.16nn0  27200  rpnnen3lem  27227  symgsssg  27511  symgfisg  27512  idomsubgmo  27617  istrlon  28340  bnj1128  29336  lsmcv2  29841  lcvat  29842  lcvexchlem4  29849  lcvexchlem5  29850  lfladd  29878  lflsub  29879  lflmul  29880  lshpkrlem4  29925  latm4  30045  omlmod1i2N  30072  cvlsupr7  30160  cvlsupr8  30161  hlatj4  30185  hlrelat3  30223  cvrval3  30224  atcvrj1  30242  atlelt  30249  2atlt  30250  2atjm  30256  3noncolr2  30260  athgt  30267  3dimlem2  30270  3dimlem4OLDN  30276  1cvratex  30284  ps-1  30288  ps-2  30289  hlatexch3N  30291  llnle  30329  atcvrlln2  30330  atcvrlln  30331  lplni2  30348  lplnle  30351  lplnnle2at  30352  lplnnlelln  30354  llncvrlpln2  30368  2llnmeqat  30382  lvolnle3at  30393  lvolnlelln  30395  4atlem0ae  30405  lneq2at  30589  lnjatN  30591  lncvrat  30593  2lnat  30595  elpaddri  30613  paddasslem2  30632  padd4N  30651  hlmod1i  30667  llnexchb2  30680  dalawlem2  30683  pclfinN  30711  pexmidlem4N  30784  pl42lem1N  30790  lhp2lt  30812  lhpexle1  30819  lhpexle2lem  30820  lhpj1  30833  lhpmcvr5N  30838  lhp2at0  30843  lhp2at0nle  30846  lhple  30853  lhpat  30854  lhpat4N  30855  4atexlemnslpq  30867  4atexlem7  30886  ltrn11  30937  ltrnle  30940  ltrnm  30942  ltrnj  30943  ltrncvr  30944  ltrnel  30950  ltrncnvel  30953  ltrncnv  30957  ltrnmw  30962  trlat  30980  trl0  30981  trlnidat  30984  trlnid  30990  ltrnatlw  30994  trlne  30996  trlval4  30999  cdlemc5  31006  cdlemd2  31010  cdlemd7  31015  cdlemd8  31016  cdlemd9  31017  cdleme0c  31024  cdleme0e  31028  cdleme0fN  31029  cdleme3g  31045  cdleme3h  31046  cdleme5  31051  cdleme11c  31072  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme0nex  31101  cdleme18a  31102  cdleme22gb  31105  cdleme20zN  31112  cdleme20y  31113  cdleme20c  31122  cdleme20k  31130  cdleme21a  31136  cdleme21b  31137  cdleme21c  31138  cdleme21ct  31140  cdleme21h  31145  cdleme22d  31154  cdleme22f  31157  cdleme26ee  31171  cdleme30a  31189  cdlemefs45eN  31242  cdleme36a  31271  cdleme36m  31272  cdleme39a  31276  cdleme42b  31289  cdleme43dN  31303  cdlemeg47rv2  31321  cdlemeg46sfg  31331  cdlemeg46rjgN  31333  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdleme48d  31346  cdleme50ltrn  31368  cdlemf1  31372  cdlemf  31374  cdlemg2dN  31401  cdlemg2fvlem  31405  cdlemg2l  31414  cdlemg7fvbwN  31418  cdlemg7aN  31436  cdlemg10c  31450  cdlemg17a  31472  cdlemg17dALTN  31475  cdlemg18a  31489  cdlemg18b  31490  cdlemg31b0a  31506  cdlemg31a  31508  cdlemg31b  31509  ltrnco  31530  cdlemg48  31548  tgrpov  31559  tendoco2  31579  tendoplco2  31590  cdlemh1  31626  cdlemk1  31642  cdlemk26b-3  31716  cdlemk27-3  31718  cdlemk28-3  31719  cdlemk34  31721  cdlemkfid1N  31732  cdlemkid3N  31744  cdlemkid4  31745  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk51  31764  tendospcanN  31835  cdlemm10N  31930  dicvaddcl  32002  dicvscacl  32003  cdlemn6  32014  dihvalcq2  32059  dihord6b  32072  dihord5apre  32074  dihglbcpreN  32112  dihjatc1  32123  dihmeetlem20N  32138  dih1dimatlem0  32140  dihglblem6  32152  dochexmidlem4  32275  mapdpglem32  32517  mapdh8ad  32591  mapdh9aOLDN  32603  hdmap11lem2  32657  hdmap14lem6  32688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator