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

Theorem simp23 1049
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 1016 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 1036 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  simpl23  1094  simpr23  1103  simp123  1148  simp223  1157  simp323  1166  funtpg  5655  omeulem1  7314  elfiun  7975  cofsmo  8730  modexp  12445  iscatd2  15642  funcoppc  15835  funcres  15856  catcisolem  16056  1stfcl  16137  2ndfcl  16138  prfcl  16143  evlfcl  16162  curf1cl  16168  curfcl  16172  hofcl  16199  pmtrprfv3  17150  mdetunilem3  19694  mdetunilem4  19695  mdetuni0  19701  mdetmul  19703  prdsxmetlem  21438  isosctrlem3  23805  isosctr  23806  f1otrg  24957  colinearalg  24996  ax5seglem6  25020  ax5seg  25024  axpasch  25027  axeuclid  25049  ogrpsub  28531  ogrpsublt  28536  rhmdvd  28635  bnj966  29805  bnj967  29806  mclspps  30272  cgrtr  30809  cgrtr3  30811  ofscom  30824  btwnxfr  30873  colinearxfr  30892  lineext  30893  brofs2  30894  brifs2  30895  fscgr  30897  linecgr  30898  btwnconn1lem1  30904  btwnconn1lem2  30905  btwnconn1lem3  30906  btwnconn1lem4  30907  btwnconn1lem5  30908  btwnconn1lem6  30909  btwnconn1lem7  30910  seglecgr12im  30927  seglecgr12  30928  segletr  30931  broutsideof3  30943  outsideofeq  30947  lineunray  30964  eqlkr  32711  omlmod1i2N  32872  cvrcmp2  32896  cvlexch2  32941  cvlexchb2  32943  cvlatexchb2  32947  cvlatexch1  32948  cvlatexch2  32949  cvlatexch3  32950  cvlsupr7  32960  cvlsupr8  32961  atnlej1  32990  atnlej2  32991  2llnneN  33020  cvratlem  33032  atcvrneN  33041  atcvrj1  33042  atlelt  33049  2atjm  33056  3noncolr2  33060  3noncolr1N  33061  hlatcon2  33063  3dimlem2  33070  3dim1  33078  3dim2  33079  1cvrat  33087  ps-1  33088  ps-2  33089  2atjlej  33090  hlatexch3N  33091  ps-2b  33093  3atlem1  33094  3atlem2  33095  3atlem6  33099  llnle  33129  2atm  33138  ps-2c  33139  lplni2  33148  lplnle  33151  lplnnle2at  33152  lplnri3N  33166  llncvrlpln2  33168  2atmat  33172  2llnjaN  33177  2llnm2N  33179  2llnm4  33181  2llnmeqat  33182  lvolnle3at  33193  4atlem0ae  33205  4atlem0be  33206  4atlem3b  33209  4atlem9  33214  4atlem10a  33215  4atlem10  33217  4atlem11a  33218  4atlem12a  33221  4at  33224  4at2  33225  lplncvrlvol2  33226  2lplnm2N  33232  2llnma1b  33397  2llnma1  33398  2llnma3r  33399  2llnma2  33400  2llnma2rN  33401  cdlema1N  33402  cdlema2N  33403  paddasslem2  33432  paddasslem15  33445  paddasslem16  33446  pmodlem1  33457  pmod2iN  33460  hlmod1i  33467  atmod2i1  33472  atmod2i2  33473  atmod3i1  33475  atmod3i2  33476  atmod4i1  33477  atmod4i2  33478  llnexchb2  33480  dalawlem3  33484  dalawlem4  33485  dalawlem5  33486  dalawlem6  33487  dalawlem7  33488  dalawlem8  33489  dalawlem9  33490  dalawlem11  33492  dalawlem13  33494  dalawlem15  33496  osumcllem7N  33573  osumcllem9N  33575  osumcllem11N  33577  pl42lem1N  33590  4atex  33687  4atex2-0aOLDN  33689  4atex2-0bOLDN  33690  4atex2-0cOLDN  33691  trlval4  33800  cdlemc5  33807  cdlemd5  33814  cdlemd6  33815  cdleme00a  33821  cdleme3g  33846  cdleme3h  33847  cdleme3  33849  cdleme4  33850  cdleme4a  33851  cdleme16aN  33871  cdleme11c  33873  cdleme11g  33877  cdleme11h  33878  cdleme12  33883  cdleme0nex  33902  cdleme18a  33903  cdleme18b  33904  cdleme18c  33905  cdleme18d  33907  cdleme20zN  33913  cdleme20y  33914  cdleme20yOLD  33915  cdleme19a  33916  cdleme19b  33917  cdleme19d  33919  cdleme19e  33920  cdleme20aN  33922  cdleme20c  33924  cdleme20d  33925  cdleme20i  33930  cdleme20j  33931  cdleme20l1  33933  cdleme20l2  33934  cdleme20m  33936  cdleme21b  33939  cdleme21c  33940  cdleme21j  33949  cdleme22aa  33952  cdleme22a  33953  cdleme22eALTN  33958  cdleme26e  33972  cdleme26fALTN  33975  cdleme26f  33976  cdleme26f2ALTN  33977  cdleme26f2  33978  cdleme27N  33982  cdleme28a  33983  cdleme28b  33984  cdleme30a  33991  cdlemefs45eN  34044  cdleme32c  34056  cdleme32e  34058  cdleme35h  34069  cdleme36a  34073  cdleme36m  34074  cdleme37m  34075  cdleme41sn3aw  34087  cdleme41sn4aw  34088  cdleme41fva11  34090  cdleme42k  34097  cdleme43cN  34104  cdleme43dN  34105  cdleme46f2g1  34107  cdlemeg47rv2  34123  cdlemeg46sfg  34133  cdlemeg46fjgN  34134  cdlemeg46rjgN  34135  cdlemeg46fjv  34136  cdlemeg46frv  34138  cdlemeg46vrg  34140  cdlemeg46rgv  34141  cdlemeg46req  34142  cdlemeg46gfv  34143  cdleme50trn2a  34163  cdlemg2fv2  34213  cdlemg4a  34221  cdlemg4e  34227  cdlemg4f  34228  cdlemg8b  34241  cdlemg8c  34242  cdlemg9a  34245  cdlemg9b  34246  cdlemg9  34247  cdlemg10a  34253  cdlemg12a  34256  cdlemg12b  34257  cdlemg12c  34258  cdlemg12  34263  cdlemg17dN  34276  cdlemg17dALTN  34277  cdlemg17e  34278  cdlemg17i  34282  cdlemg17ir  34283  cdlemg17pq  34285  cdlemg17bq  34286  cdlemg17iqN  34287  cdlemg17  34290  cdlemg18b  34292  cdlemg18c  34293  cdlemg18d  34294  cdlemg18  34295  cdlemg19  34297  cdlemg21  34299  cdlemg28a  34306  cdlemg31b0a  34308  cdlemg33b0  34314  cdlemg35  34326  cdlemg44a  34344  cdlemh  34430  cdlemi2  34432  cdlemj1  34434  cdlemk5a  34448  cdlemk5  34449  cdlemki  34454  cdlemkvcl  34455  cdlemk10  34456  cdlemksv2  34460  cdlemk7  34461  cdlemk11  34462  cdlemk12  34463  cdlemk15  34468  cdlemk16a  34469  cdlemk16  34470  cdlemk5u  34474  cdlemk6u  34475  cdlemk18  34481  cdlemk19  34482  cdlemk7u  34483  cdlemk11u  34484  cdlemk12u  34485  cdlemk21N  34486  cdlemk20  34487  cdlemkoatnle-2N  34488  cdlemk13-2N  34489  cdlemkole-2N  34490  cdlemk14-2N  34491  cdlemk15-2N  34492  cdlemk16-2N  34493  cdlemk17-2N  34494  cdlemk18-2N  34499  cdlemk19-2N  34500  cdlemk22  34506  cdlemk30  34507  cdlemk28-3  34521  cdlemk33N  34522  cdlemkfid1N  34534  cdlemkid1  34535  cdlemky  34539  cdlemk11ta  34542  cdlemk35s-id  34551  cdlemk39s-id  34553  cdlemk47  34562  cdlemk48  34563  cdlemk49  34564  cdlemk50  34565  cdlemk51  34566  cdlemk52  34567  cdlemk53a  34568  cdlemk53b  34569  cdlemk53  34570  cdlemk54  34571  cdlemk55a  34572  cdlemkyyN  34575  cdlemk43N  34576  cdlemk55u1  34578  cdlemk55u  34579  cdlemk39u1  34580  cdlemk19u1  34582  cdleml1N  34589  cdleml2N  34590  cdleml3N  34591  dia2dimlem6  34683  cdlemn2  34809  cdlemn2a  34810  cdlemn5pre  34814  cdlemn11pre  34824  dihjustlem  34830  dihjust  34831  dihmeetlem15N  34935  lclkrlem2y  35145  relexpxpnnidm  36341  uhgr2edg  39435
  Copyright terms: Public domain W3C validator