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

Theorem simp22 992
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 959 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 980 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  simpl22  1037  simpr22  1046  simp122  1091  simp222  1100  simp322  1109  elfiun  7464  cofsmo  8180  modexp  11545  funcoppc  14103  funcres  14124  catcisolem  14292  1stfcl  14325  2ndfcl  14326  prfcl  14331  evlfcl  14350  curf1cl  14356  curfcl  14360  hofcl  14387  meetle  14488  mulgdirlem  14945  prdsxmetlem  18429  isosctrlem3  20695  isosctr  20696  amgmlem  20859  ofldaddlt  24272  rhmdvd  24290  colinearalg  25880  ax5seglem6  25904  ax5seg  25908  axpasch  25911  axeuclidlem  25932  axeuclid  25933  cgrtr  25957  cgrtr3  25959  ofscom  25972  cgrextend  25973  btwnxfr  26021  colinearxfr  26040  lineext  26041  fscgr  26045  linecgr  26046  btwnconn1lem1  26052  btwnconn1lem2  26053  btwnconn1lem3  26054  btwnconn1lem4  26055  btwnconn1lem5  26056  btwnconn1lem6  26057  btwnconn1lem7  26058  seglecgr12im  26075  seglecgr12  26076  segletr  26079  broutsideof3  26091  outsideofeq  26095  lineunray  26112  linecom  26115  bnj966  29413  eqlkr  29995  lshpkrlem5  30010  omlmod1i2N  30156  cvrnbtwn3  30172  cvrcmp2  30180  cvlexch2  30225  cvlexchb2  30227  cvlatexchb2  30231  cvlatexch1  30232  cvlatexch2  30233  cvlatexch3  30234  cvlsupr7  30244  cvlsupr8  30245  atnlej1  30274  atnlej2  30275  2llnneN  30304  cvratlem  30316  atcvrneN  30325  atlelt  30333  2atjm  30340  3noncolr2  30344  3noncolr1N  30345  hlatcon2  30347  3dimlem2  30354  3dim1  30362  3dim2  30363  1cvrat  30371  ps-1  30372  ps-2  30373  2atjlej  30374  hlatexch3N  30375  ps-2b  30377  3atlem1  30378  3atlem5  30382  3atlem6  30383  2atm  30422  ps-2c  30423  lplni2  30432  lplnri3N  30450  llncvrlpln2  30452  2atmat  30456  2llnm2N  30463  2llnm3N  30464  2llnm4  30465  2llnmeqat  30466  lvolnle3at  30477  4atlem0ae  30489  4atlem0be  30490  4atlem3b  30493  4atlem9  30498  4atlem10a  30499  4atlem10  30501  4atlem11a  30502  4atlem12a  30505  4at2  30509  2lplnm2N  30516  lneq2at  30673  2llnma1b  30681  2llnma1  30682  2llnma3r  30683  2llnma2  30684  2llnma2rN  30685  cdlema1N  30686  paddasslem2  30716  paddasslem16  30730  pmodlem1  30741  pmod2iN  30744  hlmod1i  30751  atmod2i1  30756  atmod2i2  30757  atmod3i1  30759  atmod3i2  30760  atmod4i1  30761  atmod4i2  30762  llnexchb2lem  30763  llnexch2N  30765  dalawlem3  30768  dalawlem4  30769  dalawlem5  30770  dalawlem6  30771  dalawlem7  30772  dalawlem8  30773  dalawlem9  30774  dalawlem11  30776  dalawlem12  30777  dalawlem13  30778  dalawlem15  30780  osumcllem7N  30857  osumcllem9N  30859  pl42lem1N  30874  4atexlemswapqr  30958  4atex2  30972  4atex2-0bOLDN  30974  trlval4  31083  cdlemc5  31090  cdlemc6  31091  cdlemd2  31094  cdlemd4  31096  cdlemd6  31098  cdleme00a  31104  cdleme0e  31112  cdleme4  31133  cdleme4a  31134  cdleme5  31135  cdleme9  31148  cdleme16aN  31154  cdleme11c  31156  cdleme11dN  31157  cdleme11e  31158  cdleme11g  31160  cdleme11h  31161  cdleme11j  31162  cdleme11k  31163  cdleme11l  31164  cdleme11  31165  cdleme12  31166  cdleme13  31167  cdleme14  31168  cdleme15a  31169  cdleme15c  31171  cdleme16b  31174  cdleme16c  31175  cdleme16d  31176  cdleme16e  31177  cdleme16f  31178  cdleme17d1  31184  cdleme0nex  31185  cdleme18a  31186  cdleme18b  31187  cdleme18c  31188  cdleme18d  31190  cdlemednpq  31194  cdlemednuN  31195  cdleme20zN  31196  cdleme20y  31197  cdleme19a  31198  cdleme19b  31199  cdleme19d  31201  cdleme19e  31202  cdleme20aN  31204  cdleme20d  31207  cdleme20f  31209  cdleme20g  31210  cdleme20i  31212  cdleme20j  31213  cdleme20l1  31215  cdleme20l2  31216  cdleme20l  31217  cdleme20m  31218  cdleme21b  31221  cdleme21c  31222  cdleme21e  31226  cdleme21j  31231  cdleme22aa  31234  cdleme22a  31235  cdleme22b  31236  cdleme22cN  31237  cdleme22d  31238  cdleme22e  31239  cdleme22eALTN  31240  cdleme22f  31241  cdleme26fALTN  31257  cdleme26f  31258  cdleme26f2ALTN  31259  cdleme26f2  31260  cdleme27N  31264  cdleme28a  31265  cdleme28b  31266  cdleme30a  31273  cdlemefs31fv1  31319  cdleme32b  31337  cdleme32c  31338  cdleme32e  31340  cdleme35h  31351  cdleme36a  31355  cdleme36m  31356  cdleme41sn3aw  31369  cdleme41sn4aw  31370  cdleme41fva11  31372  cdleme42k  31379  cdleme43cN  31386  cdleme46f2g1  31389  cdlemeg46fjgN  31416  cdlemeg46fjv  31418  cdlemeg46frv  31420  cdlemeg46rgv  31423  cdlemeg46req  31424  cdlemeg46gfv  31425  cdleme50trn2a  31445  cdlemg4a  31503  cdlemg4d  31508  cdlemg4e  31509  cdlemg4f  31510  cdlemg8c  31524  cdlemg9a  31527  cdlemg9b  31528  cdlemg10a  31535  cdlemg10  31536  cdlemg12b  31539  cdlemg12f  31543  cdlemg12g  31544  cdlemg12  31545  cdlemg17dN  31558  cdlemg17dALTN  31559  cdlemg17e  31560  cdlemg17f  31561  cdlemg17g  31562  cdlemg17i  31564  cdlemg17ir  31565  cdlemg17pq  31567  cdlemg17bq  31568  cdlemg17iqN  31569  cdlemg17  31572  cdlemg18b  31574  cdlemg18c  31575  cdlemg18d  31576  cdlemg18  31577  cdlemg19  31579  cdlemg21  31581  cdlemg28a  31588  cdlemg31b0a  31590  cdlemg27b  31591  cdlemg33b0  31596  cdlemg28b  31598  cdlemg28  31599  cdlemg35  31608  cdlemg36  31609  cdlemg44a  31626  cdlemh  31712  cdlemi2  31714  cdlemj1  31716  tendocan  31719  cdlemk5a  31730  cdlemk5  31731  cdlemki  31736  cdlemkvcl  31737  cdlemk10  31738  cdlemksv2  31742  cdlemk7  31743  cdlemk11  31744  cdlemk12  31745  cdlemkoatnle  31746  cdlemk15  31750  cdlemk16a  31751  cdlemk16  31752  cdlemk1u  31754  cdlemk5u  31756  cdlemk6u  31757  cdlemk18  31763  cdlemk19  31764  cdlemk7u  31765  cdlemk11u  31766  cdlemk12u  31767  cdlemk21N  31768  cdlemk20  31769  cdlemkoatnle-2N  31770  cdlemk13-2N  31771  cdlemkole-2N  31772  cdlemk14-2N  31773  cdlemk15-2N  31774  cdlemk16-2N  31775  cdlemk17-2N  31776  cdlemk18-2N  31781  cdlemk19-2N  31782  cdlemk22  31788  cdlemk30  31789  cdlemkuel-3  31793  cdlemkuv2-3N  31794  cdlemk18-3N  31795  cdlemkfid1N  31816  cdlemkid1  31817  cdlemkfid3N  31820  cdlemky  31821  cdlemk11ta  31824  cdlemk47  31844  cdlemk48  31845  cdlemk49  31846  cdlemk50  31847  cdlemk51  31848  cdlemk52  31849  cdlemk53a  31850  cdlemk53  31852  cdlemk54  31853  cdlemk55a  31854  cdlemkyyN  31857  cdlemk43N  31858  cdlemk55u1  31860  cdlemk55u  31861  cdlemk39u1  31862  cdlemk19u1  31864  cdleml1N  31871  cdleml2N  31872  cdleml3N  31873  dia2dimlem6  31965  cdlemn2  32091  cdlemn2a  32092  cdlemn5pre  32096  cdlemn11a  32103  dihjustlem  32112  dihjust  32113  dihmeetlem15N  32217  lclkrlem2y  32427
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator