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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 457 . 2  |-  ( ( ch  /\  th )  ->  ch )
213ad2ant3 1019 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  simpl3l  1051  simpr3l  1057  simp13l  1111  simp23l  1117  simp33l  1123  disjss3  4446  tfisi  6671  tfrlem5  7046  omeulem1  7228  omeulem2  7229  uniinqs  7388  elfiun  7886  tcrank  8298  isfin2-2  8695  konigthlem  8939  gruen  9186  addid2  9758  mulcan  10182  mulcan2  10183  divass  10221  divdir  10226  div11  10229  divcan5  10242  ltmul1  10388  ltdiv1  10402  ltmuldiv  10411  lediv2  10431  xaddass2  11438  xlt2add  11448  xmulasslem3  11474  xadddi2  11485  expaddz  12174  expmulz  12176  resqrtcl  13046  o1add  13395  o1mul  13396  o1sub  13397  dvdsadd2b  13883  dvdsgcd  14036  rpexp12i  14118  pythagtriplem3  14197  pcpremul  14222  pceu  14225  pcqmul  14232  pcqdiv  14236  f1ocpbllem  14775  funcoppc  15098  funcres  15119  catcisolem  15287  1stfcl  15320  2ndfcl  15321  prfcl  15326  evlfcl  15345  curf1cl  15351  curfcl  15355  hofcl  15382  latjlej12  15550  latmlem12  15566  latj4  15584  latj4rot  15585  symgsssg  16288  symgfisg  16289  psgnunilem4  16318  odcong  16369  cmn4  16613  ablsub4  16619  abladdsub4  16620  lsm4  16659  abvdom  17270  abvres  17271  abvtrivd  17272  lspsolvlem  17571  lbsextlem2  17588  frlmbas3  18574  matmulcell  18714  marrepeval  18832  ma1repveval  18840  submaeval  18851  mdetunilem3  18883  mdetuni0  18890  mdetmul  18892  minmar1eval  18918  nllyrest  19753  hausflimlem  20215  tsmsxp  20392  psmetlecl  20554  xmetlecl  20584  prdsxmetlem  20606  bndth  21193  cph2ass  21394  iscau3  21452  dvres2  22051  coemullem  22381  vieta1  22442  aalioulem4  22465  cxpcn3lem  22849  angcan  22862  dchrvmasumlema  23413  logdivsum  23446  abvcxp  23528  padicabv  23543  ax5seglem3  23910  ax5seglem6  23913  axpasch  23920  axeuclid  23942  axcontlem4  23946  axcontlem8  23950  clwwlknimp  24452  gxneg  24944  gxsuc  24950  gxmodid  24957  adjlnop  26681  xreceu  27286  orngmul  27456  rhmdvd  27474  measvunilem  27823  measvunilem0  27824  measres  27833  subdivcomb1  28580  subdivcomb2  28581  cgrcomim  29216  cgrcoml  29223  cgrcomr  29224  cgrdegen  29231  segconeu  29238  btwnintr  29246  btwnexch3  29247  btwnouttr2  29249  btwnouttr  29251  btwnexch  29252  trisegint  29255  lineext  29303  linecgr  29308  lineid  29310  idinside  29311  btwnconn1lem3  29316  btwnconn1lem4  29317  btwnconn1lem7  29320  btwnconn1lem14  29327  btwnconn2  29329  midofsegid  29331  btwnoutside  29352  outsideoftr  29356  lineunray  29374  lineelsb2  29375  cnres2  29862  heibor  29920  mzpsubst  30285  pellex  30375  pellfundex  30426  pellfund14gap  30427  qirropth  30448  rmxypos  30489  congmul  30509  congsub  30512  mzpcong  30514  coprmdvdsb  30529  jm2.15nn0  30549  jm2.16nn0  30550  rpnnen3lem  30577  idomsubgmo  30760  mullimc  31158  islptre  31161  limccog  31162  mullimcf  31165  addlimc  31190  0ellimcdiv  31191  stoweidlem57  31357  fourierdlem48  31455  fourierdlem80  31487  fourierdlem113  31520  bnj1128  33125  lsmcv2  33826  lcvat  33827  lcvexchlem4  33834  lcvexchlem5  33835  lfladd  33863  lflsub  33864  lflmul  33865  lshpkrlem4  33910  latm4  34030  omlmod1i2N  34057  cvlatexch3  34135  cvlsupr7  34145  hlatj4  34170  hlrelat3  34208  cvrval3  34209  atcvrj1  34227  atlelt  34234  2atlt  34235  2atjm  34241  3noncolr2  34245  athgt  34252  3dimlem2  34255  3dimlem4  34260  3dimlem4OLDN  34261  3dim3  34265  1cvratex  34269  ps-1  34273  ps-2  34274  hlatexch3N  34276  llnle  34314  atcvrlln2  34315  atcvrlln  34316  lplni2  34333  lplnle  34336  lplnnle2at  34337  llncvrlpln2  34353  lplnexllnN  34360  2llnmeqat  34367  lvolnle3at  34378  4atlem0ae  34390  lplncvrlvol2  34411  lnjatN  34576  lncvrat  34578  cdlemblem  34589  elpaddri  34598  paddasslem2  34617  paddasslem16  34631  padd4N  34636  hlmod1i  34652  dalawlem2  34668  pclfinN  34696  pexmidlem4N  34769  pl42lem1N  34775  lhp2lt  34797  lhpexle1  34804  lhpexle2lem  34805  lhpj1  34818  lhpmcvr5N  34823  lhp2at0  34828  lhp2atnle  34829  lhp2at0nle  34831  lhple  34838  lhpat  34839  lhpat4N  34840  4atexlempnq  34851  4atexlem7  34871  4atex  34872  ltrn11  34922  ltrnle  34925  ltrnm  34927  ltrnj  34928  ltrncvr  34929  ltrnel  34935  ltrncnvel  34938  ltrncnv  34942  ltrnmw  34947  trlval2  34959  trlcnv  34961  trljat1  34962  trljat2  34963  trlat  34965  trl0  34966  trlnidat  34969  trlnid  34975  cdlemc1  34987  cdlemc2  34988  cdlemc5  34991  cdlemd2  34995  cdlemd7  35000  cdlemd8  35001  cdlemd9  35002  cdleme0e  35013  cdleme3g  35030  cdleme3h  35031  cdleme3  35033  cdleme5  35036  cdleme10  35050  cdleme11a  35056  cdleme11c  35057  cdleme11h  35062  cdleme11j  35063  cdleme0nex  35086  cdleme18a  35087  cdleme18b  35088  cdleme22gb  35090  cdleme20zN  35097  cdleme20y  35098  cdleme20c  35107  cdleme20k  35115  cdleme21a  35121  cdleme21b  35122  cdleme21c  35123  cdleme21h  35130  cdleme22b  35137  cdleme22d  35139  cdleme22f  35142  cdleme25a  35149  cdleme25c  35151  cdleme25dN  35152  cdleme26ee  35156  cdleme30a  35174  cdlemefr29bpre0N  35202  cdlemefr29clN  35203  cdlemefr32fvaN  35205  cdlemefr32fva1  35206  cdlemefs29bpre0N  35212  cdlemefs29bpre1N  35213  cdlemefs29cpre1N  35214  cdlemefs29clN  35215  cdleme43fsv1snlem  35216  cdlemefs32fvaN  35218  cdlemefs32fva1  35219  cdlemefs31fv1  35220  cdleme36a  35256  cdleme39a  35261  cdleme42a  35267  cdleme42c  35268  cdleme17d3  35292  cdleme48fv  35295  cdleme48bw  35298  cdleme48b  35299  cdlemeg46rgv  35324  cdlemeg46req  35325  cdlemeg46gfv  35326  cdleme48d  35331  cdleme50trn2a  35346  cdleme50trn2  35347  cdleme50ltrn  35353  cdlemf1  35357  cdlemf  35359  trlord  35365  cdlemg2dN  35386  cdlemg2fvlem  35390  cdlemg2l  35399  cdlemg7fvbwN  35403  cdlemg7aN  35421  cdlemg10bALTN  35432  cdlemg10c  35435  cdlemg17a  35457  cdlemg17dALTN  35460  cdlemg31b0a  35491  cdlemg31a  35493  cdlemg31b  35494  cdlemg34  35508  cdlemg36  35510  ltrnco  35515  trlcoabs2N  35518  trlcolem  35522  cdlemg48  35533  tgrpov  35544  tendoco2  35564  tendoplco2  35575  cdlemh1  35611  cdlemi1  35614  cdlemi2  35615  cdlemj3  35619  tendoid0  35621  cdlemk1  35627  cdlemk2  35628  cdlemk4  35630  cdlemk8  35634  cdlemk9  35635  cdlemk9bN  35636  cdlemk10  35639  cdlemk26b-3  35701  cdlemk26-3  35702  cdlemk28-3  35704  cdlemk37  35710  cdlemk39  35712  cdlemkfid1N  35717  cdlemkid1  35718  cdlemky  35722  cdlemkyu  35723  cdlemk19ylem  35726  cdlemk19xlem  35738  cdlemk11t  35742  cdlemk51  35749  cdlemkyyN  35758  cdleml6  35777  cdleml7  35778  cdleml8  35779  cdleml9  35780  erngdvlem4  35787  erngdvlem4-rN  35795  tendospcanN  35820  dia11N  35845  cdlemm10N  35915  dib11N  35957  dicvaddcl  35987  dicvscacl  35988  cdlemn6  35999  dihvalcq2  36044  dihopelvalcpre  36045  dihord6b  36057  dihord5apre  36059  dihmeetlem1N  36087  dihmeetlem2N  36096  dihglbcpreN  36097  dihjatc1  36108  dihmeetlem20N  36123  dih1dimatlem0  36125  dihatlat  36131  dihglblem6  36137  dochexmidlem4  36260  mapdpglem32  36502  mapdh8ad  36576  mapdh9aOLDN  36588  hdmap11lem2  36642  hdmap14lem6  36673
  Copyright terms: Public domain W3C validator