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

Theorem simp23 1040
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 1007 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 1027 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl23  1085  simpr23  1094  simp123  1139  simp223  1148  simp323  1157  funtpg  5651  omeulem1  7294  elfiun  7953  cofsmo  8706  modexp  12413  iscatd2  15586  funcoppc  15779  funcres  15800  catcisolem  16000  1stfcl  16081  2ndfcl  16082  prfcl  16087  evlfcl  16106  curf1cl  16112  curfcl  16116  hofcl  16143  pmtrprfv3  17094  mdetunilem3  19637  mdetunilem4  19638  mdetuni0  19644  mdetmul  19646  prdsxmetlem  21381  isosctrlem3  23747  isosctr  23748  f1otrg  24899  colinearalg  24938  ax5seglem6  24962  ax5seg  24966  axpasch  24969  axeuclid  24991  ogrpsub  28487  ogrpsublt  28492  rhmdvd  28592  bnj966  29763  bnj967  29764  mclspps  30230  cgrtr  30764  cgrtr3  30766  ofscom  30779  btwnxfr  30828  colinearxfr  30847  lineext  30848  brofs2  30849  brifs2  30850  fscgr  30852  linecgr  30853  btwnconn1lem1  30859  btwnconn1lem2  30860  btwnconn1lem3  30861  btwnconn1lem4  30862  btwnconn1lem5  30863  btwnconn1lem6  30864  btwnconn1lem7  30865  seglecgr12im  30882  seglecgr12  30883  segletr  30886  broutsideof3  30898  outsideofeq  30902  lineunray  30919  eqlkr  32634  omlmod1i2N  32795  cvrcmp2  32819  cvlexch2  32864  cvlexchb2  32866  cvlatexchb2  32870  cvlatexch1  32871  cvlatexch2  32872  cvlatexch3  32873  cvlsupr7  32883  cvlsupr8  32884  atnlej1  32913  atnlej2  32914  2llnneN  32943  cvratlem  32955  atcvrneN  32964  atcvrj1  32965  atlelt  32972  2atjm  32979  3noncolr2  32983  3noncolr1N  32984  hlatcon2  32986  3dimlem2  32993  3dim1  33001  3dim2  33002  1cvrat  33010  ps-1  33011  ps-2  33012  2atjlej  33013  hlatexch3N  33014  ps-2b  33016  3atlem1  33017  3atlem2  33018  3atlem6  33022  llnle  33052  2atm  33061  ps-2c  33062  lplni2  33071  lplnle  33074  lplnnle2at  33075  lplnri3N  33089  llncvrlpln2  33091  2atmat  33095  2llnjaN  33100  2llnm2N  33102  2llnm4  33104  2llnmeqat  33105  lvolnle3at  33116  4atlem0ae  33128  4atlem0be  33129  4atlem3b  33132  4atlem9  33137  4atlem10a  33138  4atlem10  33140  4atlem11a  33141  4atlem12a  33144  4at  33147  4at2  33148  lplncvrlvol2  33149  2lplnm2N  33155  2llnma1b  33320  2llnma1  33321  2llnma3r  33322  2llnma2  33323  2llnma2rN  33324  cdlema1N  33325  cdlema2N  33326  paddasslem2  33355  paddasslem15  33368  paddasslem16  33369  pmodlem1  33380  pmod2iN  33383  hlmod1i  33390  atmod2i1  33395  atmod2i2  33396  atmod3i1  33398  atmod3i2  33399  atmod4i1  33400  atmod4i2  33401  llnexchb2  33403  dalawlem3  33407  dalawlem4  33408  dalawlem5  33409  dalawlem6  33410  dalawlem7  33411  dalawlem8  33412  dalawlem9  33413  dalawlem11  33415  dalawlem13  33417  dalawlem15  33419  osumcllem7N  33496  osumcllem9N  33498  osumcllem11N  33500  pl42lem1N  33513  4atex  33610  4atex2-0aOLDN  33612  4atex2-0bOLDN  33613  4atex2-0cOLDN  33614  trlval4  33723  cdlemc5  33730  cdlemd5  33737  cdlemd6  33738  cdleme00a  33744  cdleme3g  33769  cdleme3h  33770  cdleme3  33772  cdleme4  33773  cdleme4a  33774  cdleme16aN  33794  cdleme11c  33796  cdleme11g  33800  cdleme11h  33801  cdleme12  33806  cdleme0nex  33825  cdleme18a  33826  cdleme18b  33827  cdleme18c  33828  cdleme18d  33830  cdleme20zN  33836  cdleme20y  33837  cdleme20yOLD  33838  cdleme19a  33839  cdleme19b  33840  cdleme19d  33842  cdleme19e  33843  cdleme20aN  33845  cdleme20c  33847  cdleme20d  33848  cdleme20i  33853  cdleme20j  33854  cdleme20l1  33856  cdleme20l2  33857  cdleme20m  33859  cdleme21b  33862  cdleme21c  33863  cdleme21j  33872  cdleme22aa  33875  cdleme22a  33876  cdleme22eALTN  33881  cdleme26e  33895  cdleme26fALTN  33898  cdleme26f  33899  cdleme26f2ALTN  33900  cdleme26f2  33901  cdleme27N  33905  cdleme28a  33906  cdleme28b  33907  cdleme30a  33914  cdlemefs45eN  33967  cdleme32c  33979  cdleme32e  33981  cdleme35h  33992  cdleme36a  33996  cdleme36m  33997  cdleme37m  33998  cdleme41sn3aw  34010  cdleme41sn4aw  34011  cdleme41fva11  34013  cdleme42k  34020  cdleme43cN  34027  cdleme43dN  34028  cdleme46f2g1  34030  cdlemeg47rv2  34046  cdlemeg46sfg  34056  cdlemeg46fjgN  34057  cdlemeg46rjgN  34058  cdlemeg46fjv  34059  cdlemeg46frv  34061  cdlemeg46vrg  34063  cdlemeg46rgv  34064  cdlemeg46req  34065  cdlemeg46gfv  34066  cdleme50trn2a  34086  cdlemg2fv2  34136  cdlemg4a  34144  cdlemg4e  34150  cdlemg4f  34151  cdlemg8b  34164  cdlemg8c  34165  cdlemg9a  34168  cdlemg9b  34169  cdlemg9  34170  cdlemg10a  34176  cdlemg12a  34179  cdlemg12b  34180  cdlemg12c  34181  cdlemg12  34186  cdlemg17dN  34199  cdlemg17dALTN  34200  cdlemg17e  34201  cdlemg17i  34205  cdlemg17ir  34206  cdlemg17pq  34208  cdlemg17bq  34209  cdlemg17iqN  34210  cdlemg17  34213  cdlemg18b  34215  cdlemg18c  34216  cdlemg18d  34217  cdlemg18  34218  cdlemg19  34220  cdlemg21  34222  cdlemg28a  34229  cdlemg31b0a  34231  cdlemg33b0  34237  cdlemg35  34249  cdlemg44a  34267  cdlemh  34353  cdlemi2  34355  cdlemj1  34357  cdlemk5a  34371  cdlemk5  34372  cdlemki  34377  cdlemkvcl  34378  cdlemk10  34379  cdlemksv2  34383  cdlemk7  34384  cdlemk11  34385  cdlemk12  34386  cdlemk15  34391  cdlemk16a  34392  cdlemk16  34393  cdlemk5u  34397  cdlemk6u  34398  cdlemk18  34404  cdlemk19  34405  cdlemk7u  34406  cdlemk11u  34407  cdlemk12u  34408  cdlemk21N  34409  cdlemk20  34410  cdlemkoatnle-2N  34411  cdlemk13-2N  34412  cdlemkole-2N  34413  cdlemk14-2N  34414  cdlemk15-2N  34415  cdlemk16-2N  34416  cdlemk17-2N  34417  cdlemk18-2N  34422  cdlemk19-2N  34423  cdlemk22  34429  cdlemk30  34430  cdlemk28-3  34444  cdlemk33N  34445  cdlemkfid1N  34457  cdlemkid1  34458  cdlemky  34462  cdlemk11ta  34465  cdlemk35s-id  34474  cdlemk39s-id  34476  cdlemk47  34485  cdlemk48  34486  cdlemk49  34487  cdlemk50  34488  cdlemk51  34489  cdlemk52  34490  cdlemk53a  34491  cdlemk53b  34492  cdlemk53  34493  cdlemk54  34494  cdlemk55a  34495  cdlemkyyN  34498  cdlemk43N  34499  cdlemk55u1  34501  cdlemk55u  34502  cdlemk39u1  34503  cdlemk19u1  34505  cdleml1N  34512  cdleml2N  34513  cdleml3N  34514  dia2dimlem6  34606  cdlemn2  34732  cdlemn2a  34733  cdlemn5pre  34737  cdlemn11pre  34747  dihjustlem  34753  dihjust  34754  dihmeetlem15N  34858  lclkrlem2y  35068  relexpxpnnidm  36265
  Copyright terms: Public domain W3C validator