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

Theorem simp22 1022
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp22  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )

Proof of Theorem simp22
StepHypRef Expression
1 simp2 989 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 1010 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  simpl22  1067  simpr22  1076  simp122  1121  simp222  1130  simp322  1139  elfiun  7678  cofsmo  8436  modexp  11997  funcoppc  14783  funcres  14804  catcisolem  14972  1stfcl  15005  2ndfcl  15006  prfcl  15011  evlfcl  15030  curf1cl  15036  curfcl  15040  hofcl  15067  mulgdirlem  15649  pmtrprfv3  15958  mdetunilem4  18419  mdetuni0  18425  mdetmul  18427  prdsxmetlem  19941  isosctrlem3  22216  isosctr  22217  amgmlem  22381  f1otrg  23115  colinearalg  23154  ax5seglem6  23178  ax5seg  23182  axpasch  23185  axeuclidlem  23206  axeuclid  23207  ogrpsub  26178  ogrpsublt  26183  rhmdvd  26287  cgrtr  28021  cgrtr3  28023  ofscom  28036  cgrextend  28037  btwnxfr  28085  colinearxfr  28104  lineext  28105  fscgr  28109  linecgr  28110  btwnconn1lem1  28116  btwnconn1lem2  28117  btwnconn1lem3  28118  btwnconn1lem4  28119  btwnconn1lem5  28120  btwnconn1lem6  28121  btwnconn1lem7  28122  seglecgr12im  28139  seglecgr12  28140  segletr  28143  broutsideof3  28155  outsideofeq  28159  lineunray  28176  linecom  28179  bnj966  31934  eqlkr  32741  lshpkrlem5  32756  omlmod1i2N  32902  cvrnbtwn3  32918  cvrcmp2  32926  cvlexch2  32971  cvlexchb2  32973  cvlatexchb2  32977  cvlatexch1  32978  cvlatexch2  32979  cvlatexch3  32980  cvlsupr7  32990  cvlsupr8  32991  atnlej1  33020  atnlej2  33021  2llnneN  33050  cvratlem  33062  atcvrneN  33071  atlelt  33079  2atjm  33086  3noncolr2  33090  3noncolr1N  33091  hlatcon2  33093  3dimlem2  33100  3dim1  33108  3dim2  33109  1cvrat  33117  ps-1  33118  ps-2  33119  2atjlej  33120  hlatexch3N  33121  ps-2b  33123  3atlem1  33124  3atlem5  33128  3atlem6  33129  2atm  33168  ps-2c  33169  lplni2  33178  lplnri3N  33196  llncvrlpln2  33198  2atmat  33202  2llnm2N  33209  2llnm3N  33210  2llnm4  33211  2llnmeqat  33212  lvolnle3at  33223  4atlem0ae  33235  4atlem0be  33236  4atlem3b  33239  4atlem9  33244  4atlem10a  33245  4atlem10  33247  4atlem11a  33248  4atlem12a  33251  4at2  33255  2lplnm2N  33262  lneq2at  33419  2llnma1b  33427  2llnma1  33428  2llnma3r  33429  2llnma2  33430  2llnma2rN  33431  cdlema1N  33432  paddasslem2  33462  paddasslem16  33476  pmodlem1  33487  pmod2iN  33490  hlmod1i  33497  atmod2i1  33502  atmod2i2  33503  atmod3i1  33505  atmod3i2  33506  atmod4i1  33507  atmod4i2  33508  llnexchb2lem  33509  llnexch2N  33511  dalawlem3  33514  dalawlem4  33515  dalawlem5  33516  dalawlem6  33517  dalawlem7  33518  dalawlem8  33519  dalawlem9  33520  dalawlem11  33522  dalawlem12  33523  dalawlem13  33524  dalawlem15  33526  osumcllem7N  33603  osumcllem9N  33605  pl42lem1N  33620  4atexlemswapqr  33704  4atex2  33718  4atex2-0bOLDN  33720  trlval4  33829  cdlemc5  33836  cdlemc6  33837  cdlemd2  33840  cdlemd4  33842  cdlemd6  33844  cdleme00a  33850  cdleme0e  33858  cdleme4  33879  cdleme4a  33880  cdleme5  33881  cdleme9  33894  cdleme16aN  33900  cdleme11c  33902  cdleme11dN  33903  cdleme11e  33904  cdleme11g  33906  cdleme11h  33907  cdleme11j  33908  cdleme11k  33909  cdleme11l  33910  cdleme11  33911  cdleme12  33912  cdleme13  33913  cdleme14  33914  cdleme15a  33915  cdleme15c  33917  cdleme16b  33920  cdleme16c  33921  cdleme16d  33922  cdleme16e  33923  cdleme16f  33924  cdleme17d1  33930  cdleme0nex  33931  cdleme18a  33932  cdleme18b  33933  cdleme18c  33934  cdleme18d  33936  cdlemednpq  33940  cdlemednuN  33941  cdleme20zN  33942  cdleme20y  33943  cdleme19a  33944  cdleme19b  33945  cdleme19d  33947  cdleme19e  33948  cdleme20aN  33950  cdleme20d  33953  cdleme20f  33955  cdleme20g  33956  cdleme20i  33958  cdleme20j  33959  cdleme20l1  33961  cdleme20l2  33962  cdleme20l  33963  cdleme20m  33964  cdleme21b  33967  cdleme21c  33968  cdleme21e  33972  cdleme21j  33977  cdleme22aa  33980  cdleme22a  33981  cdleme22b  33982  cdleme22cN  33983  cdleme22d  33984  cdleme22e  33985  cdleme22eALTN  33986  cdleme22f  33987  cdleme26fALTN  34003  cdleme26f  34004  cdleme26f2ALTN  34005  cdleme26f2  34006  cdleme27N  34010  cdleme28a  34011  cdleme28b  34012  cdleme30a  34019  cdlemefs31fv1  34065  cdleme32b  34083  cdleme32c  34084  cdleme32e  34086  cdleme35h  34097  cdleme36a  34101  cdleme36m  34102  cdleme41sn3aw  34115  cdleme41sn4aw  34116  cdleme41fva11  34118  cdleme42k  34125  cdleme43cN  34132  cdleme46f2g1  34135  cdlemeg46fjgN  34162  cdlemeg46fjv  34164  cdlemeg46frv  34166  cdlemeg46rgv  34169  cdlemeg46req  34170  cdlemeg46gfv  34171  cdleme50trn2a  34191  cdlemg4a  34249  cdlemg4d  34254  cdlemg4e  34255  cdlemg4f  34256  cdlemg8c  34270  cdlemg9a  34273  cdlemg9b  34274  cdlemg10a  34281  cdlemg10  34282  cdlemg12b  34285  cdlemg12f  34289  cdlemg12g  34290  cdlemg12  34291  cdlemg17dN  34304  cdlemg17dALTN  34305  cdlemg17e  34306  cdlemg17f  34307  cdlemg17g  34308  cdlemg17i  34310  cdlemg17ir  34311  cdlemg17pq  34313  cdlemg17bq  34314  cdlemg17iqN  34315  cdlemg17  34318  cdlemg18b  34320  cdlemg18c  34321  cdlemg18d  34322  cdlemg18  34323  cdlemg19  34325  cdlemg21  34327  cdlemg28a  34334  cdlemg31b0a  34336  cdlemg27b  34337  cdlemg33b0  34342  cdlemg28b  34344  cdlemg28  34345  cdlemg35  34354  cdlemg36  34355  cdlemg44a  34372  cdlemh  34458  cdlemi2  34460  cdlemj1  34462  tendocan  34465  cdlemk5a  34476  cdlemk5  34477  cdlemki  34482  cdlemkvcl  34483  cdlemk10  34484  cdlemksv2  34488  cdlemk7  34489  cdlemk11  34490  cdlemk12  34491  cdlemkoatnle  34492  cdlemk15  34496  cdlemk16a  34497  cdlemk16  34498  cdlemk1u  34500  cdlemk5u  34502  cdlemk6u  34503  cdlemk18  34509  cdlemk19  34510  cdlemk7u  34511  cdlemk11u  34512  cdlemk12u  34513  cdlemk21N  34514  cdlemk20  34515  cdlemkoatnle-2N  34516  cdlemk13-2N  34517  cdlemkole-2N  34518  cdlemk14-2N  34519  cdlemk15-2N  34520  cdlemk16-2N  34521  cdlemk17-2N  34522  cdlemk18-2N  34527  cdlemk19-2N  34528  cdlemk22  34534  cdlemk30  34535  cdlemkuel-3  34539  cdlemkuv2-3N  34540  cdlemk18-3N  34541  cdlemkfid1N  34562  cdlemkid1  34563  cdlemkfid3N  34566  cdlemky  34567  cdlemk11ta  34570  cdlemk47  34590  cdlemk48  34591  cdlemk49  34592  cdlemk50  34593  cdlemk51  34594  cdlemk52  34595  cdlemk53a  34596  cdlemk53  34598  cdlemk54  34599  cdlemk55a  34600  cdlemkyyN  34603  cdlemk43N  34604  cdlemk55u1  34606  cdlemk55u  34607  cdlemk39u1  34608  cdlemk19u1  34610  cdleml1N  34617  cdleml2N  34618  cdleml3N  34619  dia2dimlem6  34711  cdlemn2  34837  cdlemn2a  34838  cdlemn5pre  34842  cdlemn11a  34849  dihjustlem  34858  dihjust  34859  dihmeetlem15N  34963  lclkrlem2y  35173
  Copyright terms: Public domain W3C validator