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

Theorem simp23 990
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 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl23  1035  simpr23  1044  simp123  1089  simp223  1098  simp323  1107  omeulem1  6596  elfiun  7199  cofsmo  7911  modexp  11252  iscatd2  13599  funcoppc  13765  funcres  13786  catcisolem  13954  1stfcl  13987  2ndfcl  13988  prfcl  13993  evlfcl  14012  curf1cl  14018  curfcl  14022  hofcl  14049  meetle  14150  prdsxmetlem  17948  isosctrlem3  20136  isosctr  20137  colinearalg  24610  ax5seglem6  24634  ax5seg  24638  axpasch  24641  axeuclid  24663  cgrtr  24687  cgrtr3  24689  ofscom  24702  btwnxfr  24751  colinearxfr  24770  lineext  24771  brofs2  24772  brifs2  24773  fscgr  24775  linecgr  24776  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem7  24788  seglecgr12im  24805  seglecgr12  24806  segletr  24809  broutsideof3  24821  outsideofeq  24825  lineunray  24842  cmpmorass  26069  bisig0  26165  elhaltdp  26170  bnj966  29292  bnj967  29293  eqlkr  29911  omlmod1i2N  30072  cvrcmp2  30096  cvlexch2  30141  cvlexchb2  30143  cvlatexchb2  30147  cvlatexch1  30148  cvlatexch2  30149  cvlatexch3  30150  cvlsupr7  30160  cvlsupr8  30161  atnlej1  30190  atnlej2  30191  2llnneN  30220  cvratlem  30232  atcvrneN  30241  atcvrj1  30242  atlelt  30249  2atjm  30256  3noncolr2  30260  3noncolr1N  30261  hlatcon2  30263  3dimlem2  30270  3dim1  30278  3dim2  30279  1cvrat  30287  ps-1  30288  ps-2  30289  2atjlej  30290  hlatexch3N  30291  ps-2b  30293  3atlem1  30294  3atlem2  30295  3atlem6  30299  llnle  30329  2atm  30338  ps-2c  30339  lplni2  30348  lplnle  30351  lplnnle2at  30352  lplnri3N  30366  llncvrlpln2  30368  2atmat  30372  2llnjaN  30377  2llnm2N  30379  2llnm4  30381  2llnmeqat  30382  lvolnle3at  30393  4atlem0ae  30405  4atlem0be  30406  4atlem3b  30409  4atlem9  30414  4atlem10a  30415  4atlem10  30417  4atlem11a  30418  4atlem12a  30421  4at  30424  4at2  30425  lplncvrlvol2  30426  2lplnm2N  30432  2llnma1b  30597  2llnma1  30598  2llnma3r  30599  2llnma2  30600  2llnma2rN  30601  cdlema1N  30602  cdlema2N  30603  paddasslem2  30632  paddasslem15  30645  paddasslem16  30646  pmodlem1  30657  pmod2iN  30660  hlmod1i  30667  atmod2i1  30672  atmod2i2  30673  atmod3i1  30675  atmod3i2  30676  atmod4i1  30677  atmod4i2  30678  llnexchb2  30680  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem9  30690  dalawlem11  30692  dalawlem13  30694  dalawlem15  30696  osumcllem7N  30773  osumcllem9N  30775  osumcllem11N  30777  pl42lem1N  30790  4atex  30887  4atex2-0aOLDN  30889  4atex2-0bOLDN  30890  4atex2-0cOLDN  30891  trlval4  30999  cdlemc5  31006  cdlemd5  31013  cdlemd6  31014  cdleme00a  31020  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme4  31049  cdleme4a  31050  cdleme16aN  31070  cdleme11c  31072  cdleme11g  31076  cdleme11h  31077  cdleme12  31082  cdleme0nex  31101  cdleme18a  31102  cdleme18b  31103  cdleme18c  31104  cdleme18d  31106  cdleme20zN  31112  cdleme20y  31113  cdleme19a  31114  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20aN  31120  cdleme20c  31122  cdleme20d  31123  cdleme20i  31128  cdleme20j  31129  cdleme20l1  31131  cdleme20l2  31132  cdleme20m  31134  cdleme21b  31137  cdleme21c  31138  cdleme21j  31147  cdleme22aa  31150  cdleme22a  31151  cdleme22eALTN  31156  cdleme26e  31170  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme27N  31180  cdleme28a  31181  cdleme28b  31182  cdleme30a  31189  cdlemefs45eN  31242  cdleme32c  31254  cdleme32e  31256  cdleme35h  31267  cdleme36a  31271  cdleme36m  31272  cdleme37m  31273  cdleme41sn3aw  31285  cdleme41sn4aw  31286  cdleme41fva11  31288  cdleme42k  31295  cdleme43cN  31302  cdleme43dN  31303  cdleme46f2g1  31305  cdlemeg47rv2  31321  cdlemeg46sfg  31331  cdlemeg46fjgN  31332  cdlemeg46rjgN  31333  cdlemeg46fjv  31334  cdlemeg46frv  31336  cdlemeg46vrg  31338  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdleme50trn2a  31361  cdlemg2fv2  31411  cdlemg4a  31419  cdlemg4e  31425  cdlemg4f  31426  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg9b  31444  cdlemg9  31445  cdlemg10a  31451  cdlemg12a  31454  cdlemg12b  31455  cdlemg12c  31456  cdlemg12  31461  cdlemg17dN  31474  cdlemg17dALTN  31475  cdlemg17e  31476  cdlemg17i  31480  cdlemg17ir  31481  cdlemg17pq  31483  cdlemg17bq  31484  cdlemg17iqN  31485  cdlemg17  31488  cdlemg18b  31490  cdlemg18c  31491  cdlemg18d  31492  cdlemg18  31493  cdlemg19  31495  cdlemg21  31497  cdlemg28a  31504  cdlemg31b0a  31506  cdlemg33b0  31512  cdlemg35  31524  cdlemg44a  31542  cdlemh  31628  cdlemi2  31630  cdlemj1  31632  cdlemk5a  31646  cdlemk5  31647  cdlemki  31652  cdlemkvcl  31653  cdlemk10  31654  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemk15  31666  cdlemk16a  31667  cdlemk16  31668  cdlemk5u  31672  cdlemk6u  31673  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk11u  31682  cdlemk12u  31683  cdlemk21N  31684  cdlemk20  31685  cdlemkoatnle-2N  31686  cdlemk13-2N  31687  cdlemkole-2N  31688  cdlemk14-2N  31689  cdlemk15-2N  31690  cdlemk16-2N  31691  cdlemk17-2N  31692  cdlemk18-2N  31697  cdlemk19-2N  31698  cdlemk22  31704  cdlemk30  31705  cdlemk28-3  31719  cdlemk33N  31720  cdlemkfid1N  31732  cdlemkid1  31733  cdlemky  31737  cdlemk11ta  31740  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk47  31760  cdlemk48  31761  cdlemk49  31762  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdlemk53b  31767  cdlemk53  31768  cdlemk54  31769  cdlemk55a  31770  cdlemkyyN  31773  cdlemk43N  31774  cdlemk55u1  31776  cdlemk55u  31777  cdlemk39u1  31778  cdlemk19u1  31780  cdleml1N  31787  cdleml2N  31788  cdleml3N  31789  dia2dimlem6  31881  cdlemn2  32007  cdlemn2a  32008  cdlemn5pre  32012  cdlemn11pre  32022  dihjustlem  32028  dihjust  32029  dihmeetlem15N  32133  lclkrlem2y  32343
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