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

Theorem simp23 1026
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp23  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )

Proof of Theorem simp23
StepHypRef Expression
1 simp3 993 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 1013 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  simpl23  1071  simpr23  1080  simp123  1125  simp223  1134  simp323  1143  funtpg  5629  omeulem1  7221  elfiun  7879  cofsmo  8638  modexp  12256  iscatd2  14925  funcoppc  15091  funcres  15112  catcisolem  15280  1stfcl  15313  2ndfcl  15314  prfcl  15319  evlfcl  15338  curf1cl  15344  curfcl  15348  hofcl  15375  pmtrprfv3  16268  mdetunilem3  18876  mdetunilem4  18877  mdetuni0  18883  mdetmul  18885  prdsxmetlem  20599  isosctrlem3  22875  isosctr  22876  f1otrg  23843  colinearalg  23882  ax5seglem6  23906  ax5seg  23910  axpasch  23913  axeuclid  23935  ogrpsub  27355  ogrpsublt  27360  rhmdvd  27460  cgrtr  29205  cgrtr3  29207  ofscom  29220  btwnxfr  29269  colinearxfr  29288  lineext  29289  brofs2  29290  brifs2  29291  fscgr  29293  linecgr  29294  btwnconn1lem1  29300  btwnconn1lem2  29301  btwnconn1lem3  29302  btwnconn1lem4  29303  btwnconn1lem5  29304  btwnconn1lem6  29305  btwnconn1lem7  29306  seglecgr12im  29323  seglecgr12  29324  segletr  29327  broutsideof3  29339  outsideofeq  29343  lineunray  29360  bnj966  32956  bnj967  32957  eqlkr  33771  omlmod1i2N  33932  cvrcmp2  33956  cvlexch2  34001  cvlexchb2  34003  cvlatexchb2  34007  cvlatexch1  34008  cvlatexch2  34009  cvlatexch3  34010  cvlsupr7  34020  cvlsupr8  34021  atnlej1  34050  atnlej2  34051  2llnneN  34080  cvratlem  34092  atcvrneN  34101  atcvrj1  34102  atlelt  34109  2atjm  34116  3noncolr2  34120  3noncolr1N  34121  hlatcon2  34123  3dimlem2  34130  3dim1  34138  3dim2  34139  1cvrat  34147  ps-1  34148  ps-2  34149  2atjlej  34150  hlatexch3N  34151  ps-2b  34153  3atlem1  34154  3atlem2  34155  3atlem6  34159  llnle  34189  2atm  34198  ps-2c  34199  lplni2  34208  lplnle  34211  lplnnle2at  34212  lplnri3N  34226  llncvrlpln2  34228  2atmat  34232  2llnjaN  34237  2llnm2N  34239  2llnm4  34241  2llnmeqat  34242  lvolnle3at  34253  4atlem0ae  34265  4atlem0be  34266  4atlem3b  34269  4atlem9  34274  4atlem10a  34275  4atlem10  34277  4atlem11a  34278  4atlem12a  34281  4at  34284  4at2  34285  lplncvrlvol2  34286  2lplnm2N  34292  2llnma1b  34457  2llnma1  34458  2llnma3r  34459  2llnma2  34460  2llnma2rN  34461  cdlema1N  34462  cdlema2N  34463  paddasslem2  34492  paddasslem15  34505  paddasslem16  34506  pmodlem1  34517  pmod2iN  34520  hlmod1i  34527  atmod2i1  34532  atmod2i2  34533  atmod3i1  34535  atmod3i2  34536  atmod4i1  34537  atmod4i2  34538  llnexchb2  34540  dalawlem3  34544  dalawlem4  34545  dalawlem5  34546  dalawlem6  34547  dalawlem7  34548  dalawlem8  34549  dalawlem9  34550  dalawlem11  34552  dalawlem13  34554  dalawlem15  34556  osumcllem7N  34633  osumcllem9N  34635  osumcllem11N  34637  pl42lem1N  34650  4atex  34747  4atex2-0aOLDN  34749  4atex2-0bOLDN  34750  4atex2-0cOLDN  34751  trlval4  34859  cdlemc5  34866  cdlemd5  34873  cdlemd6  34874  cdleme00a  34880  cdleme3g  34905  cdleme3h  34906  cdleme3  34908  cdleme4  34909  cdleme4a  34910  cdleme16aN  34930  cdleme11c  34932  cdleme11g  34936  cdleme11h  34937  cdleme12  34942  cdleme0nex  34961  cdleme18a  34962  cdleme18b  34963  cdleme18c  34964  cdleme18d  34966  cdleme20zN  34972  cdleme20y  34973  cdleme19a  34974  cdleme19b  34975  cdleme19d  34977  cdleme19e  34978  cdleme20aN  34980  cdleme20c  34982  cdleme20d  34983  cdleme20i  34988  cdleme20j  34989  cdleme20l1  34991  cdleme20l2  34992  cdleme20m  34994  cdleme21b  34997  cdleme21c  34998  cdleme21j  35007  cdleme22aa  35010  cdleme22a  35011  cdleme22eALTN  35016  cdleme26e  35030  cdleme26fALTN  35033  cdleme26f  35034  cdleme26f2ALTN  35035  cdleme26f2  35036  cdleme27N  35040  cdleme28a  35041  cdleme28b  35042  cdleme30a  35049  cdlemefs45eN  35102  cdleme32c  35114  cdleme32e  35116  cdleme35h  35127  cdleme36a  35131  cdleme36m  35132  cdleme37m  35133  cdleme41sn3aw  35145  cdleme41sn4aw  35146  cdleme41fva11  35148  cdleme42k  35155  cdleme43cN  35162  cdleme43dN  35163  cdleme46f2g1  35165  cdlemeg47rv2  35181  cdlemeg46sfg  35191  cdlemeg46fjgN  35192  cdlemeg46rjgN  35193  cdlemeg46fjv  35194  cdlemeg46frv  35196  cdlemeg46vrg  35198  cdlemeg46rgv  35199  cdlemeg46req  35200  cdlemeg46gfv  35201  cdleme50trn2a  35221  cdlemg2fv2  35271  cdlemg4a  35279  cdlemg4e  35285  cdlemg4f  35286  cdlemg8b  35299  cdlemg8c  35300  cdlemg9a  35303  cdlemg9b  35304  cdlemg9  35305  cdlemg10a  35311  cdlemg12a  35314  cdlemg12b  35315  cdlemg12c  35316  cdlemg12  35321  cdlemg17dN  35334  cdlemg17dALTN  35335  cdlemg17e  35336  cdlemg17i  35340  cdlemg17ir  35341  cdlemg17pq  35343  cdlemg17bq  35344  cdlemg17iqN  35345  cdlemg17  35348  cdlemg18b  35350  cdlemg18c  35351  cdlemg18d  35352  cdlemg18  35353  cdlemg19  35355  cdlemg21  35357  cdlemg28a  35364  cdlemg31b0a  35366  cdlemg33b0  35372  cdlemg35  35384  cdlemg44a  35402  cdlemh  35488  cdlemi2  35490  cdlemj1  35492  cdlemk5a  35506  cdlemk5  35507  cdlemki  35512  cdlemkvcl  35513  cdlemk10  35514  cdlemksv2  35518  cdlemk7  35519  cdlemk11  35520  cdlemk12  35521  cdlemk15  35526  cdlemk16a  35527  cdlemk16  35528  cdlemk5u  35532  cdlemk6u  35533  cdlemk18  35539  cdlemk19  35540  cdlemk7u  35541  cdlemk11u  35542  cdlemk12u  35543  cdlemk21N  35544  cdlemk20  35545  cdlemkoatnle-2N  35546  cdlemk13-2N  35547  cdlemkole-2N  35548  cdlemk14-2N  35549  cdlemk15-2N  35550  cdlemk16-2N  35551  cdlemk17-2N  35552  cdlemk18-2N  35557  cdlemk19-2N  35558  cdlemk22  35564  cdlemk30  35565  cdlemk28-3  35579  cdlemk33N  35580  cdlemkfid1N  35592  cdlemkid1  35593  cdlemky  35597  cdlemk11ta  35600  cdlemk35s-id  35609  cdlemk39s-id  35611  cdlemk47  35620  cdlemk48  35621  cdlemk49  35622  cdlemk50  35623  cdlemk51  35624  cdlemk52  35625  cdlemk53a  35626  cdlemk53b  35627  cdlemk53  35628  cdlemk54  35629  cdlemk55a  35630  cdlemkyyN  35633  cdlemk43N  35634  cdlemk55u1  35636  cdlemk55u  35637  cdlemk39u1  35638  cdlemk19u1  35640  cdleml1N  35647  cdleml2N  35648  cdleml3N  35649  dia2dimlem6  35741  cdlemn2  35867  cdlemn2a  35868  cdlemn5pre  35872  cdlemn11pre  35882  dihjustlem  35888  dihjust  35889  dihmeetlem15N  35993  lclkrlem2y  36203
  Copyright terms: Public domain W3C validator