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

Theorem simp22 1041
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 1008 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 1029 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 984
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 189  df-an 373  df-3an 986
This theorem is referenced by:  simpl22  1086  simpr22  1095  simp122  1140  simp222  1149  simp322  1158  elfiun  7941  cofsmo  8696  modexp  12404  funcoppc  15773  funcres  15794  catcisolem  15994  1stfcl  16075  2ndfcl  16076  prfcl  16081  evlfcl  16100  curf1cl  16106  curfcl  16110  hofcl  16137  mulgdirlem  16775  pmtrprfv3  17088  mdetunilem4  19633  mdetuni0  19639  mdetmul  19641  prdsxmetlem  21376  isosctrlem3  23742  isosctr  23743  amgmlem  23908  f1otrg  24894  colinearalg  24933  ax5seglem6  24957  ax5seg  24961  axpasch  24964  axeuclidlem  24985  axeuclid  24986  ogrpsub  28473  ogrpaddlt  28474  ogrpsublt  28478  rhmdvd  28577  bnj966  29748  mclspps  30215  cgrtr  30752  cgrtr3  30754  ofscom  30767  cgrextend  30768  btwnxfr  30816  colinearxfr  30835  lineext  30836  fscgr  30840  linecgr  30841  btwnconn1lem1  30847  btwnconn1lem2  30848  btwnconn1lem3  30849  btwnconn1lem4  30850  btwnconn1lem5  30851  btwnconn1lem6  30852  btwnconn1lem7  30853  seglecgr12im  30870  seglecgr12  30871  segletr  30874  broutsideof3  30886  outsideofeq  30890  lineunray  30907  linecom  30910  eqlkr  32659  lshpkrlem5  32674  omlmod1i2N  32820  cvrnbtwn3  32836  cvrcmp2  32844  cvlexch2  32889  cvlexchb2  32891  cvlatexchb2  32895  cvlatexch1  32896  cvlatexch2  32897  cvlatexch3  32898  cvlsupr7  32908  cvlsupr8  32909  atnlej1  32938  atnlej2  32939  2llnneN  32968  cvratlem  32980  atcvrneN  32989  atlelt  32997  2atjm  33004  3noncolr2  33008  3noncolr1N  33009  hlatcon2  33011  3dimlem2  33018  3dim1  33026  3dim2  33027  1cvrat  33035  ps-1  33036  ps-2  33037  2atjlej  33038  hlatexch3N  33039  ps-2b  33041  3atlem1  33042  3atlem5  33046  3atlem6  33047  2atm  33086  ps-2c  33087  lplni2  33096  lplnri3N  33114  llncvrlpln2  33116  2atmat  33120  2llnm2N  33127  2llnm3N  33128  2llnm4  33129  2llnmeqat  33130  lvolnle3at  33141  4atlem0ae  33153  4atlem0be  33154  4atlem3b  33157  4atlem9  33162  4atlem10a  33163  4atlem10  33165  4atlem11a  33166  4atlem12a  33169  4at2  33173  2lplnm2N  33180  lneq2at  33337  2llnma1b  33345  2llnma1  33346  2llnma3r  33347  2llnma2  33348  2llnma2rN  33349  cdlema1N  33350  paddasslem2  33380  paddasslem16  33394  pmodlem1  33405  pmod2iN  33408  hlmod1i  33415  atmod2i1  33420  atmod2i2  33421  atmod3i1  33423  atmod3i2  33424  atmod4i1  33425  atmod4i2  33426  llnexchb2lem  33427  llnexch2N  33429  dalawlem3  33432  dalawlem4  33433  dalawlem5  33434  dalawlem6  33435  dalawlem7  33436  dalawlem8  33437  dalawlem9  33438  dalawlem11  33440  dalawlem12  33441  dalawlem13  33442  dalawlem15  33444  osumcllem7N  33521  osumcllem9N  33523  pl42lem1N  33538  4atexlemswapqr  33622  4atex2  33636  4atex2-0bOLDN  33638  trlval4  33748  cdlemc5  33755  cdlemc6  33756  cdlemd2  33759  cdlemd4  33761  cdlemd6  33763  cdleme00a  33769  cdleme0e  33777  cdleme4  33798  cdleme4a  33799  cdleme5  33800  cdleme9  33813  cdleme16aN  33819  cdleme11c  33821  cdleme11dN  33822  cdleme11e  33823  cdleme11g  33825  cdleme11h  33826  cdleme11j  33827  cdleme11k  33828  cdleme11l  33829  cdleme11  33830  cdleme12  33831  cdleme13  33832  cdleme14  33833  cdleme15a  33834  cdleme15c  33836  cdleme16b  33839  cdleme16c  33840  cdleme16d  33841  cdleme16e  33842  cdleme16f  33843  cdleme17d1  33849  cdleme0nex  33850  cdleme18a  33851  cdleme18b  33852  cdleme18c  33853  cdleme18d  33855  cdlemednpq  33859  cdlemednuN  33860  cdleme20zN  33861  cdleme20y  33862  cdleme20yOLD  33863  cdleme19a  33864  cdleme19b  33865  cdleme19d  33867  cdleme19e  33868  cdleme20aN  33870  cdleme20d  33873  cdleme20f  33875  cdleme20g  33876  cdleme20i  33878  cdleme20j  33879  cdleme20l1  33881  cdleme20l2  33882  cdleme20l  33883  cdleme20m  33884  cdleme21b  33887  cdleme21c  33888  cdleme21e  33892  cdleme21j  33897  cdleme22aa  33900  cdleme22a  33901  cdleme22b  33902  cdleme22cN  33903  cdleme22d  33904  cdleme22e  33905  cdleme22eALTN  33906  cdleme22f  33907  cdleme26fALTN  33923  cdleme26f  33924  cdleme26f2ALTN  33925  cdleme26f2  33926  cdleme27N  33930  cdleme28a  33931  cdleme28b  33932  cdleme30a  33939  cdlemefs31fv1  33985  cdleme32b  34003  cdleme32c  34004  cdleme32e  34006  cdleme35h  34017  cdleme36a  34021  cdleme36m  34022  cdleme41sn3aw  34035  cdleme41sn4aw  34036  cdleme41fva11  34038  cdleme42k  34045  cdleme43cN  34052  cdleme46f2g1  34055  cdlemeg46fjgN  34082  cdlemeg46fjv  34084  cdlemeg46frv  34086  cdlemeg46rgv  34089  cdlemeg46req  34090  cdlemeg46gfv  34091  cdleme50trn2a  34111  cdlemg4a  34169  cdlemg4d  34174  cdlemg4e  34175  cdlemg4f  34176  cdlemg8c  34190  cdlemg9a  34193  cdlemg9b  34194  cdlemg10a  34201  cdlemg10  34202  cdlemg12b  34205  cdlemg12f  34209  cdlemg12g  34210  cdlemg12  34211  cdlemg17dN  34224  cdlemg17dALTN  34225  cdlemg17e  34226  cdlemg17f  34227  cdlemg17g  34228  cdlemg17i  34230  cdlemg17ir  34231  cdlemg17pq  34233  cdlemg17bq  34234  cdlemg17iqN  34235  cdlemg17  34238  cdlemg18b  34240  cdlemg18c  34241  cdlemg18d  34242  cdlemg18  34243  cdlemg19  34245  cdlemg21  34247  cdlemg28a  34254  cdlemg31b0a  34256  cdlemg27b  34257  cdlemg33b0  34262  cdlemg28b  34264  cdlemg28  34265  cdlemg35  34274  cdlemg36  34275  cdlemg44a  34292  cdlemh  34378  cdlemi2  34380  cdlemj1  34382  tendocan  34385  cdlemk5a  34396  cdlemk5  34397  cdlemki  34402  cdlemkvcl  34403  cdlemk10  34404  cdlemksv2  34408  cdlemk7  34409  cdlemk11  34410  cdlemk12  34411  cdlemkoatnle  34412  cdlemk15  34416  cdlemk16a  34417  cdlemk16  34418  cdlemk1u  34420  cdlemk5u  34422  cdlemk6u  34423  cdlemk18  34429  cdlemk19  34430  cdlemk7u  34431  cdlemk11u  34432  cdlemk12u  34433  cdlemk21N  34434  cdlemk20  34435  cdlemkoatnle-2N  34436  cdlemk13-2N  34437  cdlemkole-2N  34438  cdlemk14-2N  34439  cdlemk15-2N  34440  cdlemk16-2N  34441  cdlemk17-2N  34442  cdlemk18-2N  34447  cdlemk19-2N  34448  cdlemk22  34454  cdlemk30  34455  cdlemkuel-3  34459  cdlemkuv2-3N  34460  cdlemk18-3N  34461  cdlemkfid1N  34482  cdlemkid1  34483  cdlemkfid3N  34486  cdlemky  34487  cdlemk11ta  34490  cdlemk47  34510  cdlemk48  34511  cdlemk49  34512  cdlemk50  34513  cdlemk51  34514  cdlemk52  34515  cdlemk53a  34516  cdlemk53  34518  cdlemk54  34519  cdlemk55a  34520  cdlemkyyN  34523  cdlemk43N  34524  cdlemk55u1  34526  cdlemk55u  34527  cdlemk39u1  34528  cdlemk19u1  34530  cdleml1N  34537  cdleml2N  34538  cdleml3N  34539  dia2dimlem6  34631  cdlemn2  34757  cdlemn2a  34758  cdlemn5pre  34762  cdlemn11a  34769  dihjustlem  34778  dihjust  34779  dihmeetlem15N  34883  lclkrlem2y  35093  relexpmulnn  36295
  Copyright terms: Public domain W3C validator