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

Theorem simp23 1032
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 999 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 1019 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 976
This theorem is referenced by:  simpl23  1077  simpr23  1086  simp123  1131  simp223  1140  simp323  1149  funtpg  5628  omeulem1  7233  elfiun  7892  cofsmo  8652  modexp  12282  iscatd2  15059  funcoppc  15222  funcres  15243  catcisolem  15411  1stfcl  15444  2ndfcl  15445  prfcl  15450  evlfcl  15469  curf1cl  15475  curfcl  15479  hofcl  15506  pmtrprfv3  16457  mdetunilem3  19093  mdetunilem4  19094  mdetuni0  19100  mdetmul  19102  prdsxmetlem  20848  isosctrlem3  23130  isosctr  23131  f1otrg  24150  colinearalg  24189  ax5seglem6  24213  ax5seg  24217  axpasch  24220  axeuclid  24242  ogrpsub  27684  ogrpsublt  27689  rhmdvd  27788  mclspps  28921  cgrtr  29617  cgrtr3  29619  ofscom  29632  btwnxfr  29681  colinearxfr  29700  lineext  29701  brofs2  29702  brifs2  29703  fscgr  29705  linecgr  29706  btwnconn1lem1  29712  btwnconn1lem2  29713  btwnconn1lem3  29714  btwnconn1lem4  29715  btwnconn1lem5  29716  btwnconn1lem6  29717  btwnconn1lem7  29718  seglecgr12im  29735  seglecgr12  29736  segletr  29739  broutsideof3  29751  outsideofeq  29755  lineunray  29772  bnj966  33735  bnj967  33736  eqlkr  34564  omlmod1i2N  34725  cvrcmp2  34749  cvlexch2  34794  cvlexchb2  34796  cvlatexchb2  34800  cvlatexch1  34801  cvlatexch2  34802  cvlatexch3  34803  cvlsupr7  34813  cvlsupr8  34814  atnlej1  34843  atnlej2  34844  2llnneN  34873  cvratlem  34885  atcvrneN  34894  atcvrj1  34895  atlelt  34902  2atjm  34909  3noncolr2  34913  3noncolr1N  34914  hlatcon2  34916  3dimlem2  34923  3dim1  34931  3dim2  34932  1cvrat  34940  ps-1  34941  ps-2  34942  2atjlej  34943  hlatexch3N  34944  ps-2b  34946  3atlem1  34947  3atlem2  34948  3atlem6  34952  llnle  34982  2atm  34991  ps-2c  34992  lplni2  35001  lplnle  35004  lplnnle2at  35005  lplnri3N  35019  llncvrlpln2  35021  2atmat  35025  2llnjaN  35030  2llnm2N  35032  2llnm4  35034  2llnmeqat  35035  lvolnle3at  35046  4atlem0ae  35058  4atlem0be  35059  4atlem3b  35062  4atlem9  35067  4atlem10a  35068  4atlem10  35070  4atlem11a  35071  4atlem12a  35074  4at  35077  4at2  35078  lplncvrlvol2  35079  2lplnm2N  35085  2llnma1b  35250  2llnma1  35251  2llnma3r  35252  2llnma2  35253  2llnma2rN  35254  cdlema1N  35255  cdlema2N  35256  paddasslem2  35285  paddasslem15  35298  paddasslem16  35299  pmodlem1  35310  pmod2iN  35313  hlmod1i  35320  atmod2i1  35325  atmod2i2  35326  atmod3i1  35328  atmod3i2  35329  atmod4i1  35330  atmod4i2  35331  llnexchb2  35333  dalawlem3  35337  dalawlem4  35338  dalawlem5  35339  dalawlem6  35340  dalawlem7  35341  dalawlem8  35342  dalawlem9  35343  dalawlem11  35345  dalawlem13  35347  dalawlem15  35349  osumcllem7N  35426  osumcllem9N  35428  osumcllem11N  35430  pl42lem1N  35443  4atex  35540  4atex2-0aOLDN  35542  4atex2-0bOLDN  35543  4atex2-0cOLDN  35544  trlval4  35653  cdlemc5  35660  cdlemd5  35667  cdlemd6  35668  cdleme00a  35674  cdleme3g  35699  cdleme3h  35700  cdleme3  35702  cdleme4  35703  cdleme4a  35704  cdleme16aN  35724  cdleme11c  35726  cdleme11g  35730  cdleme11h  35731  cdleme12  35736  cdleme0nex  35755  cdleme18a  35756  cdleme18b  35757  cdleme18c  35758  cdleme18d  35760  cdleme20zN  35766  cdleme20y  35767  cdleme20yOLD  35768  cdleme19a  35769  cdleme19b  35770  cdleme19d  35772  cdleme19e  35773  cdleme20aN  35775  cdleme20c  35777  cdleme20d  35778  cdleme20i  35783  cdleme20j  35784  cdleme20l1  35786  cdleme20l2  35787  cdleme20m  35789  cdleme21b  35792  cdleme21c  35793  cdleme21j  35802  cdleme22aa  35805  cdleme22a  35806  cdleme22eALTN  35811  cdleme26e  35825  cdleme26fALTN  35828  cdleme26f  35829  cdleme26f2ALTN  35830  cdleme26f2  35831  cdleme27N  35835  cdleme28a  35836  cdleme28b  35837  cdleme30a  35844  cdlemefs45eN  35897  cdleme32c  35909  cdleme32e  35911  cdleme35h  35922  cdleme36a  35926  cdleme36m  35927  cdleme37m  35928  cdleme41sn3aw  35940  cdleme41sn4aw  35941  cdleme41fva11  35943  cdleme42k  35950  cdleme43cN  35957  cdleme43dN  35958  cdleme46f2g1  35960  cdlemeg47rv2  35976  cdlemeg46sfg  35986  cdlemeg46fjgN  35987  cdlemeg46rjgN  35988  cdlemeg46fjv  35989  cdlemeg46frv  35991  cdlemeg46vrg  35993  cdlemeg46rgv  35994  cdlemeg46req  35995  cdlemeg46gfv  35996  cdleme50trn2a  36016  cdlemg2fv2  36066  cdlemg4a  36074  cdlemg4e  36080  cdlemg4f  36081  cdlemg8b  36094  cdlemg8c  36095  cdlemg9a  36098  cdlemg9b  36099  cdlemg9  36100  cdlemg10a  36106  cdlemg12a  36109  cdlemg12b  36110  cdlemg12c  36111  cdlemg12  36116  cdlemg17dN  36129  cdlemg17dALTN  36130  cdlemg17e  36131  cdlemg17i  36135  cdlemg17ir  36136  cdlemg17pq  36138  cdlemg17bq  36139  cdlemg17iqN  36140  cdlemg17  36143  cdlemg18b  36145  cdlemg18c  36146  cdlemg18d  36147  cdlemg18  36148  cdlemg19  36150  cdlemg21  36152  cdlemg28a  36159  cdlemg31b0a  36161  cdlemg33b0  36167  cdlemg35  36179  cdlemg44a  36197  cdlemh  36283  cdlemi2  36285  cdlemj1  36287  cdlemk5a  36301  cdlemk5  36302  cdlemki  36307  cdlemkvcl  36308  cdlemk10  36309  cdlemksv2  36313  cdlemk7  36314  cdlemk11  36315  cdlemk12  36316  cdlemk15  36321  cdlemk16a  36322  cdlemk16  36323  cdlemk5u  36327  cdlemk6u  36328  cdlemk18  36334  cdlemk19  36335  cdlemk7u  36336  cdlemk11u  36337  cdlemk12u  36338  cdlemk21N  36339  cdlemk20  36340  cdlemkoatnle-2N  36341  cdlemk13-2N  36342  cdlemkole-2N  36343  cdlemk14-2N  36344  cdlemk15-2N  36345  cdlemk16-2N  36346  cdlemk17-2N  36347  cdlemk18-2N  36352  cdlemk19-2N  36353  cdlemk22  36359  cdlemk30  36360  cdlemk28-3  36374  cdlemk33N  36375  cdlemkfid1N  36387  cdlemkid1  36388  cdlemky  36392  cdlemk11ta  36395  cdlemk35s-id  36404  cdlemk39s-id  36406  cdlemk47  36415  cdlemk48  36416  cdlemk49  36417  cdlemk50  36418  cdlemk51  36419  cdlemk52  36420  cdlemk53a  36421  cdlemk53b  36422  cdlemk53  36423  cdlemk54  36424  cdlemk55a  36425  cdlemkyyN  36428  cdlemk43N  36429  cdlemk55u1  36431  cdlemk55u  36432  cdlemk39u1  36433  cdlemk19u1  36435  cdleml1N  36442  cdleml2N  36443  cdleml3N  36444  dia2dimlem6  36536  cdlemn2  36662  cdlemn2a  36663  cdlemn5pre  36667  cdlemn11pre  36677  dihjustlem  36683  dihjust  36684  dihmeetlem15N  36788  lclkrlem2y  36998
  Copyright terms: Public domain W3C validator