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

Theorem simp22 991
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 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl22  1036  simpr22  1045  simp122  1090  simp222  1099  simp322  1108  elfiun  7363  cofsmo  8075  modexp  11434  funcoppc  13992  funcres  14013  catcisolem  14181  1stfcl  14214  2ndfcl  14215  prfcl  14220  evlfcl  14239  curf1cl  14245  curfcl  14249  hofcl  14276  meetle  14377  mulgdirlem  14834  prdsxmetlem  18299  isosctrlem3  20524  isosctr  20525  amgmlem  20688  ofldaddlt  24060  rhmdvd  24068  colinearalg  25556  ax5seglem6  25580  ax5seg  25584  axpasch  25587  axeuclidlem  25608  axeuclid  25609  cgrtr  25633  cgrtr3  25635  ofscom  25648  cgrextend  25649  btwnxfr  25697  colinearxfr  25716  lineext  25717  fscgr  25721  linecgr  25722  btwnconn1lem1  25728  btwnconn1lem2  25729  btwnconn1lem3  25730  btwnconn1lem4  25731  btwnconn1lem5  25732  btwnconn1lem6  25733  btwnconn1lem7  25734  seglecgr12im  25751  seglecgr12  25752  segletr  25755  broutsideof3  25767  outsideofeq  25771  lineunray  25788  linecom  25791  bnj966  28646  eqlkr  29265  lshpkrlem5  29280  omlmod1i2N  29426  cvrnbtwn3  29442  cvrcmp2  29450  cvlexch2  29495  cvlexchb2  29497  cvlatexchb2  29501  cvlatexch1  29502  cvlatexch2  29503  cvlatexch3  29504  cvlsupr7  29514  cvlsupr8  29515  atnlej1  29544  atnlej2  29545  2llnneN  29574  cvratlem  29586  atcvrneN  29595  atlelt  29603  2atjm  29610  3noncolr2  29614  3noncolr1N  29615  hlatcon2  29617  3dimlem2  29624  3dim1  29632  3dim2  29633  1cvrat  29641  ps-1  29642  ps-2  29643  2atjlej  29644  hlatexch3N  29645  ps-2b  29647  3atlem1  29648  3atlem5  29652  3atlem6  29653  2atm  29692  ps-2c  29693  lplni2  29702  lplnri3N  29720  llncvrlpln2  29722  2atmat  29726  2llnm2N  29733  2llnm3N  29734  2llnm4  29735  2llnmeqat  29736  lvolnle3at  29747  4atlem0ae  29759  4atlem0be  29760  4atlem3b  29763  4atlem9  29768  4atlem10a  29769  4atlem10  29771  4atlem11a  29772  4atlem12a  29775  4at2  29779  2lplnm2N  29786  lneq2at  29943  2llnma1b  29951  2llnma1  29952  2llnma3r  29953  2llnma2  29954  2llnma2rN  29955  cdlema1N  29956  paddasslem2  29986  paddasslem16  30000  pmodlem1  30011  pmod2iN  30014  hlmod1i  30021  atmod2i1  30026  atmod2i2  30027  atmod3i1  30029  atmod3i2  30030  atmod4i1  30031  atmod4i2  30032  llnexchb2lem  30033  llnexch2N  30035  dalawlem3  30038  dalawlem4  30039  dalawlem5  30040  dalawlem6  30041  dalawlem7  30042  dalawlem8  30043  dalawlem9  30044  dalawlem11  30046  dalawlem12  30047  dalawlem13  30048  dalawlem15  30050  osumcllem7N  30127  osumcllem9N  30129  pl42lem1N  30144  4atexlemswapqr  30228  4atex2  30242  4atex2-0bOLDN  30244  trlval4  30353  cdlemc5  30360  cdlemc6  30361  cdlemd2  30364  cdlemd4  30366  cdlemd6  30368  cdleme00a  30374  cdleme0e  30382  cdleme4  30403  cdleme4a  30404  cdleme5  30405  cdleme9  30418  cdleme16aN  30424  cdleme11c  30426  cdleme11dN  30427  cdleme11e  30428  cdleme11g  30430  cdleme11h  30431  cdleme11j  30432  cdleme11k  30433  cdleme11l  30434  cdleme11  30435  cdleme12  30436  cdleme13  30437  cdleme14  30438  cdleme15a  30439  cdleme15c  30441  cdleme16b  30444  cdleme16c  30445  cdleme16d  30446  cdleme16e  30447  cdleme16f  30448  cdleme17d1  30454  cdleme0nex  30455  cdleme18a  30456  cdleme18b  30457  cdleme18c  30458  cdleme18d  30460  cdlemednpq  30464  cdlemednuN  30465  cdleme20zN  30466  cdleme20y  30467  cdleme19a  30468  cdleme19b  30469  cdleme19d  30471  cdleme19e  30472  cdleme20aN  30474  cdleme20d  30477  cdleme20f  30479  cdleme20g  30480  cdleme20i  30482  cdleme20j  30483  cdleme20l1  30485  cdleme20l2  30486  cdleme20l  30487  cdleme20m  30488  cdleme21b  30491  cdleme21c  30492  cdleme21e  30496  cdleme21j  30501  cdleme22aa  30504  cdleme22a  30505  cdleme22b  30506  cdleme22cN  30507  cdleme22d  30508  cdleme22e  30509  cdleme22eALTN  30510  cdleme22f  30511  cdleme26fALTN  30527  cdleme26f  30528  cdleme26f2ALTN  30529  cdleme26f2  30530  cdleme27N  30534  cdleme28a  30535  cdleme28b  30536  cdleme30a  30543  cdlemefs31fv1  30589  cdleme32b  30607  cdleme32c  30608  cdleme32e  30610  cdleme35h  30621  cdleme36a  30625  cdleme36m  30626  cdleme41sn3aw  30639  cdleme41sn4aw  30640  cdleme41fva11  30642  cdleme42k  30649  cdleme43cN  30656  cdleme46f2g1  30659  cdlemeg46fjgN  30686  cdlemeg46fjv  30688  cdlemeg46frv  30690  cdlemeg46rgv  30693  cdlemeg46req  30694  cdlemeg46gfv  30695  cdleme50trn2a  30715  cdlemg4a  30773  cdlemg4d  30778  cdlemg4e  30779  cdlemg4f  30780  cdlemg8c  30794  cdlemg9a  30797  cdlemg9b  30798  cdlemg10a  30805  cdlemg10  30806  cdlemg12b  30809  cdlemg12f  30813  cdlemg12g  30814  cdlemg12  30815  cdlemg17dN  30828  cdlemg17dALTN  30829  cdlemg17e  30830  cdlemg17f  30831  cdlemg17g  30832  cdlemg17i  30834  cdlemg17ir  30835  cdlemg17pq  30837  cdlemg17bq  30838  cdlemg17iqN  30839  cdlemg17  30842  cdlemg18b  30844  cdlemg18c  30845  cdlemg18d  30846  cdlemg18  30847  cdlemg19  30849  cdlemg21  30851  cdlemg28a  30858  cdlemg31b0a  30860  cdlemg27b  30861  cdlemg33b0  30866  cdlemg28b  30868  cdlemg28  30869  cdlemg35  30878  cdlemg36  30879  cdlemg44a  30896  cdlemh  30982  cdlemi2  30984  cdlemj1  30986  tendocan  30989  cdlemk5a  31000  cdlemk5  31001  cdlemki  31006  cdlemkvcl  31007  cdlemk10  31008  cdlemksv2  31012  cdlemk7  31013  cdlemk11  31014  cdlemk12  31015  cdlemkoatnle  31016  cdlemk15  31020  cdlemk16a  31021  cdlemk16  31022  cdlemk1u  31024  cdlemk5u  31026  cdlemk6u  31027  cdlemk18  31033  cdlemk19  31034  cdlemk7u  31035  cdlemk11u  31036  cdlemk12u  31037  cdlemk21N  31038  cdlemk20  31039  cdlemkoatnle-2N  31040  cdlemk13-2N  31041  cdlemkole-2N  31042  cdlemk14-2N  31043  cdlemk15-2N  31044  cdlemk16-2N  31045  cdlemk17-2N  31046  cdlemk18-2N  31051  cdlemk19-2N  31052  cdlemk22  31058  cdlemk30  31059  cdlemkuel-3  31063  cdlemkuv2-3N  31064  cdlemk18-3N  31065  cdlemkfid1N  31086  cdlemkid1  31087  cdlemkfid3N  31090  cdlemky  31091  cdlemk11ta  31094  cdlemk47  31114  cdlemk48  31115  cdlemk49  31116  cdlemk50  31117  cdlemk51  31118  cdlemk52  31119  cdlemk53a  31120  cdlemk53  31122  cdlemk54  31123  cdlemk55a  31124  cdlemkyyN  31127  cdlemk43N  31128  cdlemk55u1  31130  cdlemk55u  31131  cdlemk39u1  31132  cdlemk19u1  31134  cdleml1N  31141  cdleml2N  31142  cdleml3N  31143  dia2dimlem6  31235  cdlemn2  31361  cdlemn2a  31362  cdlemn5pre  31366  cdlemn11a  31373  dihjustlem  31382  dihjust  31383  dihmeetlem15N  31487  lclkrlem2y  31697
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator