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  7291  elfiun  7950  cofsmo  8697  modexp  12404  iscatd2  15538  funcoppc  15731  funcres  15752  catcisolem  15952  1stfcl  16033  2ndfcl  16034  prfcl  16039  evlfcl  16058  curf1cl  16064  curfcl  16068  hofcl  16095  pmtrprfv3  17046  mdetunilem3  19570  mdetunilem4  19571  mdetuni0  19577  mdetmul  19579  prdsxmetlem  21314  isosctrlem3  23614  isosctr  23615  f1otrg  24747  colinearalg  24786  ax5seglem6  24810  ax5seg  24814  axpasch  24817  axeuclid  24839  ogrpsub  28318  ogrpsublt  28323  rhmdvd  28423  bnj966  29543  bnj967  29544  mclspps  30010  cgrtr  30544  cgrtr3  30546  ofscom  30559  btwnxfr  30608  colinearxfr  30627  lineext  30628  brofs2  30629  brifs2  30630  fscgr  30632  linecgr  30633  btwnconn1lem1  30639  btwnconn1lem2  30640  btwnconn1lem3  30641  btwnconn1lem4  30642  btwnconn1lem5  30643  btwnconn1lem6  30644  btwnconn1lem7  30645  seglecgr12im  30662  seglecgr12  30663  segletr  30666  broutsideof3  30678  outsideofeq  30682  lineunray  30699  eqlkr  32373  omlmod1i2N  32534  cvrcmp2  32558  cvlexch2  32603  cvlexchb2  32605  cvlatexchb2  32609  cvlatexch1  32610  cvlatexch2  32611  cvlatexch3  32612  cvlsupr7  32622  cvlsupr8  32623  atnlej1  32652  atnlej2  32653  2llnneN  32682  cvratlem  32694  atcvrneN  32703  atcvrj1  32704  atlelt  32711  2atjm  32718  3noncolr2  32722  3noncolr1N  32723  hlatcon2  32725  3dimlem2  32732  3dim1  32740  3dim2  32741  1cvrat  32749  ps-1  32750  ps-2  32751  2atjlej  32752  hlatexch3N  32753  ps-2b  32755  3atlem1  32756  3atlem2  32757  3atlem6  32761  llnle  32791  2atm  32800  ps-2c  32801  lplni2  32810  lplnle  32813  lplnnle2at  32814  lplnri3N  32828  llncvrlpln2  32830  2atmat  32834  2llnjaN  32839  2llnm2N  32841  2llnm4  32843  2llnmeqat  32844  lvolnle3at  32855  4atlem0ae  32867  4atlem0be  32868  4atlem3b  32871  4atlem9  32876  4atlem10a  32877  4atlem10  32879  4atlem11a  32880  4atlem12a  32883  4at  32886  4at2  32887  lplncvrlvol2  32888  2lplnm2N  32894  2llnma1b  33059  2llnma1  33060  2llnma3r  33061  2llnma2  33062  2llnma2rN  33063  cdlema1N  33064  cdlema2N  33065  paddasslem2  33094  paddasslem15  33107  paddasslem16  33108  pmodlem1  33119  pmod2iN  33122  hlmod1i  33129  atmod2i1  33134  atmod2i2  33135  atmod3i1  33137  atmod3i2  33138  atmod4i1  33139  atmod4i2  33140  llnexchb2  33142  dalawlem3  33146  dalawlem4  33147  dalawlem5  33148  dalawlem6  33149  dalawlem7  33150  dalawlem8  33151  dalawlem9  33152  dalawlem11  33154  dalawlem13  33156  dalawlem15  33158  osumcllem7N  33235  osumcllem9N  33237  osumcllem11N  33239  pl42lem1N  33252  4atex  33349  4atex2-0aOLDN  33351  4atex2-0bOLDN  33352  4atex2-0cOLDN  33353  trlval4  33462  cdlemc5  33469  cdlemd5  33476  cdlemd6  33477  cdleme00a  33483  cdleme3g  33508  cdleme3h  33509  cdleme3  33511  cdleme4  33512  cdleme4a  33513  cdleme16aN  33533  cdleme11c  33535  cdleme11g  33539  cdleme11h  33540  cdleme12  33545  cdleme0nex  33564  cdleme18a  33565  cdleme18b  33566  cdleme18c  33567  cdleme18d  33569  cdleme20zN  33575  cdleme20y  33576  cdleme20yOLD  33577  cdleme19a  33578  cdleme19b  33579  cdleme19d  33581  cdleme19e  33582  cdleme20aN  33584  cdleme20c  33586  cdleme20d  33587  cdleme20i  33592  cdleme20j  33593  cdleme20l1  33595  cdleme20l2  33596  cdleme20m  33598  cdleme21b  33601  cdleme21c  33602  cdleme21j  33611  cdleme22aa  33614  cdleme22a  33615  cdleme22eALTN  33620  cdleme26e  33634  cdleme26fALTN  33637  cdleme26f  33638  cdleme26f2ALTN  33639  cdleme26f2  33640  cdleme27N  33644  cdleme28a  33645  cdleme28b  33646  cdleme30a  33653  cdlemefs45eN  33706  cdleme32c  33718  cdleme32e  33720  cdleme35h  33731  cdleme36a  33735  cdleme36m  33736  cdleme37m  33737  cdleme41sn3aw  33749  cdleme41sn4aw  33750  cdleme41fva11  33752  cdleme42k  33759  cdleme43cN  33766  cdleme43dN  33767  cdleme46f2g1  33769  cdlemeg47rv2  33785  cdlemeg46sfg  33795  cdlemeg46fjgN  33796  cdlemeg46rjgN  33797  cdlemeg46fjv  33798  cdlemeg46frv  33800  cdlemeg46vrg  33802  cdlemeg46rgv  33803  cdlemeg46req  33804  cdlemeg46gfv  33805  cdleme50trn2a  33825  cdlemg2fv2  33875  cdlemg4a  33883  cdlemg4e  33889  cdlemg4f  33890  cdlemg8b  33903  cdlemg8c  33904  cdlemg9a  33907  cdlemg9b  33908  cdlemg9  33909  cdlemg10a  33915  cdlemg12a  33918  cdlemg12b  33919  cdlemg12c  33920  cdlemg12  33925  cdlemg17dN  33938  cdlemg17dALTN  33939  cdlemg17e  33940  cdlemg17i  33944  cdlemg17ir  33945  cdlemg17pq  33947  cdlemg17bq  33948  cdlemg17iqN  33949  cdlemg17  33952  cdlemg18b  33954  cdlemg18c  33955  cdlemg18d  33956  cdlemg18  33957  cdlemg19  33959  cdlemg21  33961  cdlemg28a  33968  cdlemg31b0a  33970  cdlemg33b0  33976  cdlemg35  33988  cdlemg44a  34006  cdlemh  34092  cdlemi2  34094  cdlemj1  34096  cdlemk5a  34110  cdlemk5  34111  cdlemki  34116  cdlemkvcl  34117  cdlemk10  34118  cdlemksv2  34122  cdlemk7  34123  cdlemk11  34124  cdlemk12  34125  cdlemk15  34130  cdlemk16a  34131  cdlemk16  34132  cdlemk5u  34136  cdlemk6u  34137  cdlemk18  34143  cdlemk19  34144  cdlemk7u  34145  cdlemk11u  34146  cdlemk12u  34147  cdlemk21N  34148  cdlemk20  34149  cdlemkoatnle-2N  34150  cdlemk13-2N  34151  cdlemkole-2N  34152  cdlemk14-2N  34153  cdlemk15-2N  34154  cdlemk16-2N  34155  cdlemk17-2N  34156  cdlemk18-2N  34161  cdlemk19-2N  34162  cdlemk22  34168  cdlemk30  34169  cdlemk28-3  34183  cdlemk33N  34184  cdlemkfid1N  34196  cdlemkid1  34197  cdlemky  34201  cdlemk11ta  34204  cdlemk35s-id  34213  cdlemk39s-id  34215  cdlemk47  34224  cdlemk48  34225  cdlemk49  34226  cdlemk50  34227  cdlemk51  34228  cdlemk52  34229  cdlemk53a  34230  cdlemk53b  34231  cdlemk53  34232  cdlemk54  34233  cdlemk55a  34234  cdlemkyyN  34237  cdlemk43N  34238  cdlemk55u1  34240  cdlemk55u  34241  cdlemk39u1  34242  cdlemk19u1  34244  cdleml1N  34251  cdleml2N  34252  cdleml3N  34253  dia2dimlem6  34345  cdlemn2  34471  cdlemn2a  34472  cdlemn5pre  34476  cdlemn11pre  34486  dihjustlem  34492  dihjust  34493  dihmeetlem15N  34597  lclkrlem2y  34807  relexpxpnnidm  35933
  Copyright terms: Public domain W3C validator