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

Theorem simp3r 986
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 448 . 2  |-  ( ( ch  /\  th )  ->  th )
213ad2ant3 980 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl3r  1013  simpr3r  1019  simp13r  1073  simp23r  1079  simp33r  1085  disjss3  4152  tfisi  4778  f1oiso2  6011  omeulem1  6761  omeulem2  6762  elfiun  7370  isfin2-2  8132  addid2  9181  mulcan  9591  mulcan2  9592  divass  9628  divdir  9633  div11  9636  ltdiv1  9806  ltmuldiv  9812  lediv2  9832  xaddass2  10761  xlt2add  10771  expaddz  11351  expmulz  11353  resqrex  11983  resqrcl  11986  o1add  12334  o1mul  12335  o1sub  12336  dvdsgcd  12970  rpexp12i  13049  pythagtriplem4  13120  pythagtriplem11  13126  pythagtriplem13  13128  pcpremul  13144  pceu  13147  pcqmul  13154  pcqdiv  13158  f1ocpbllem  13676  funcoppc  13999  funcres  14020  catcisolem  14188  1stfcl  14221  2ndfcl  14222  prfcl  14227  evlfcl  14246  curf1cl  14252  curfcl  14256  hofcl  14283  latjlej12  14423  latmlem12  14439  latj4  14457  latj4rot  14458  odcong  15114  cmn4  15358  ablsub4  15364  abladdsub4  15365  lsm4  15402  abvdom  15853  abvtrivd  15855  lspsolvlem  16141  lbsextlem2  16158  hausflimlem  17932  xmetlecl  18285  prdsxmetlem  18306  xblcntr  18337  bndth  18854  cph2ass  19046  iscau3  19102  dvres2  19666  coemullem  20035  vieta1  20096  aalioulem4  20119  cxpcn3lem  20498  angcan  20511  divsqrsumlem  20685  dchrmusumlema  21054  dchrvmasumlema  21061  dchrisum0lema  21075  logdivsum  21094  padicabv  21191  gxnval  21696  gxnn0mul  21713  adjlnop  23437  xreceu  24006  ofldmul  24065  rhmdvd  24075  measvunilem  24360  measvuni  24362  ax5seglem3  25584  ax5seglem6  25587  axpasch  25594  axeuclid  25616  axcontlem4  25620  axcontlem8  25624  cgrcomim  25637  cgrcoml  25644  cgrcomr  25645  cgrdegen  25652  segconeu  25659  btwnintr  25667  btwnexch3  25668  btwnouttr2  25670  btwnouttr  25672  btwnexch  25673  ifscgr  25692  lineext  25724  linecgr  25729  lineid  25731  idinside  25732  btwnconn1lem3  25737  btwnconn1lem4  25738  btwnconn1lem14  25748  btwnconn2  25750  btwnconn3  25751  midofsegid  25752  btwnoutside  25773  outsideoftr  25777  lineunray  25795  lineelsb2  25796  itg2addnclem  25957  itg2addnc  25959  cnres2  26163  heibor  26221  mzpmfp  26495  mzpsubst  26496  pellex  26589  pellfundex  26640  pellfund14gap  26641  qirropth  26662  rmxypos  26703  congmul  26723  congsub  26726  mzpcong  26728  coprmdvdsb  26743  jm2.15nn0  26765  jm2.16nn0  26766  rpnnen3lem  26793  symgsssg  27077  symgfisg  27078  idomsubgmo  27183  bnj1128  28697  lsmcv2  29144  lcvat  29145  lcvexchlem4  29152  lcvexchlem5  29153  lfladd  29181  lflsub  29182  lflmul  29183  lshpkrlem4  29228  latm4  29348  omlmod1i2N  29375  cvlsupr7  29463  cvlsupr8  29464  hlatj4  29488  hlrelat3  29526  cvrval3  29527  atcvrj1  29545  atlelt  29552  2atlt  29553  2atjm  29559  3noncolr2  29563  athgt  29570  3dimlem2  29573  3dimlem4OLDN  29579  1cvratex  29587  ps-1  29591  ps-2  29592  hlatexch3N  29594  llnle  29632  atcvrlln2  29633  atcvrlln  29634  lplni2  29651  lplnle  29654  lplnnle2at  29655  lplnnlelln  29657  llncvrlpln2  29671  2llnmeqat  29685  lvolnle3at  29696  lvolnlelln  29698  4atlem0ae  29708  lneq2at  29892  lnjatN  29894  lncvrat  29896  2lnat  29898  elpaddri  29916  paddasslem2  29935  padd4N  29954  hlmod1i  29970  llnexchb2  29983  dalawlem2  29986  pclfinN  30014  pexmidlem4N  30087  pl42lem1N  30093  lhp2lt  30115  lhpexle1  30122  lhpexle2lem  30123  lhpj1  30136  lhpmcvr5N  30141  lhp2at0  30146  lhp2at0nle  30149  lhple  30156  lhpat  30157  lhpat4N  30158  4atexlemnslpq  30170  4atexlem7  30189  ltrn11  30240  ltrnle  30243  ltrnm  30245  ltrnj  30246  ltrncvr  30247  ltrnel  30253  ltrncnvel  30256  ltrncnv  30260  ltrnmw  30265  trlat  30283  trl0  30284  trlnidat  30287  trlnid  30293  ltrnatlw  30297  trlne  30299  trlval4  30302  cdlemc5  30309  cdlemd2  30313  cdlemd7  30318  cdlemd8  30319  cdlemd9  30320  cdleme0c  30327  cdleme0e  30331  cdleme0fN  30332  cdleme3g  30348  cdleme3h  30349  cdleme5  30354  cdleme11c  30375  cdleme11h  30380  cdleme11j  30381  cdleme11k  30382  cdleme0nex  30404  cdleme18a  30405  cdleme22gb  30408  cdleme20zN  30415  cdleme20y  30416  cdleme20c  30425  cdleme20k  30433  cdleme21a  30439  cdleme21b  30440  cdleme21c  30441  cdleme21ct  30443  cdleme21h  30448  cdleme22d  30457  cdleme22f  30460  cdleme26ee  30474  cdleme30a  30492  cdlemefs45eN  30545  cdleme36a  30574  cdleme36m  30575  cdleme39a  30579  cdleme42b  30592  cdleme43dN  30606  cdlemeg47rv2  30624  cdlemeg46sfg  30634  cdlemeg46rjgN  30636  cdlemeg46rgv  30642  cdlemeg46req  30643  cdlemeg46gfv  30644  cdleme48d  30649  cdleme50ltrn  30671  cdlemf1  30675  cdlemf  30677  cdlemg2dN  30704  cdlemg2fvlem  30708  cdlemg2l  30717  cdlemg7fvbwN  30721  cdlemg7aN  30739  cdlemg10c  30753  cdlemg17a  30775  cdlemg17dALTN  30778  cdlemg18a  30792  cdlemg18b  30793  cdlemg31b0a  30809  cdlemg31a  30811  cdlemg31b  30812  ltrnco  30833  cdlemg48  30851  tgrpov  30862  tendoco2  30882  tendoplco2  30893  cdlemh1  30929  cdlemk1  30945  cdlemk26b-3  31019  cdlemk27-3  31021  cdlemk28-3  31022  cdlemk34  31024  cdlemkfid1N  31035  cdlemkid3N  31047  cdlemkid4  31048  cdlemk35s-id  31052  cdlemk39s-id  31054  cdlemk51  31067  tendospcanN  31138  cdlemm10N  31233  dicvaddcl  31305  dicvscacl  31306  cdlemn6  31317  dihvalcq2  31362  dihord6b  31375  dihord5apre  31377  dihglbcpreN  31415  dihjatc1  31426  dihmeetlem20N  31441  dih1dimatlem0  31443  dihglblem6  31455  dochexmidlem4  31578  mapdpglem32  31820  mapdh8ad  31894  mapdh9aOLDN  31906  hdmap11lem2  31960  hdmap14lem6  31991
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator