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

Theorem simp22 1025
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 992 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 1013 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  simpl22  1070  simpr22  1079  simp122  1124  simp222  1133  simp322  1142  elfiun  7879  cofsmo  8638  modexp  12256  funcoppc  15091  funcres  15112  catcisolem  15280  1stfcl  15313  2ndfcl  15314  prfcl  15319  evlfcl  15338  curf1cl  15344  curfcl  15348  hofcl  15375  mulgdirlem  15959  pmtrprfv3  16268  mdetunilem4  18877  mdetuni0  18883  mdetmul  18885  prdsxmetlem  20599  isosctrlem3  22875  isosctr  22876  amgmlem  23040  f1otrg  23843  colinearalg  23882  ax5seglem6  23906  ax5seg  23910  axpasch  23913  axeuclidlem  23934  axeuclid  23935  ogrpsub  27355  ogrpsublt  27360  rhmdvd  27460  cgrtr  29205  cgrtr3  29207  ofscom  29220  cgrextend  29221  btwnxfr  29269  colinearxfr  29288  lineext  29289  fscgr  29293  linecgr  29294  btwnconn1lem1  29300  btwnconn1lem2  29301  btwnconn1lem3  29302  btwnconn1lem4  29303  btwnconn1lem5  29304  btwnconn1lem6  29305  btwnconn1lem7  29306  seglecgr12im  29323  seglecgr12  29324  segletr  29327  broutsideof3  29339  outsideofeq  29343  lineunray  29360  linecom  29363  bnj966  32956  eqlkr  33771  lshpkrlem5  33786  omlmod1i2N  33932  cvrnbtwn3  33948  cvrcmp2  33956  cvlexch2  34001  cvlexchb2  34003  cvlatexchb2  34007  cvlatexch1  34008  cvlatexch2  34009  cvlatexch3  34010  cvlsupr7  34020  cvlsupr8  34021  atnlej1  34050  atnlej2  34051  2llnneN  34080  cvratlem  34092  atcvrneN  34101  atlelt  34109  2atjm  34116  3noncolr2  34120  3noncolr1N  34121  hlatcon2  34123  3dimlem2  34130  3dim1  34138  3dim2  34139  1cvrat  34147  ps-1  34148  ps-2  34149  2atjlej  34150  hlatexch3N  34151  ps-2b  34153  3atlem1  34154  3atlem5  34158  3atlem6  34159  2atm  34198  ps-2c  34199  lplni2  34208  lplnri3N  34226  llncvrlpln2  34228  2atmat  34232  2llnm2N  34239  2llnm3N  34240  2llnm4  34241  2llnmeqat  34242  lvolnle3at  34253  4atlem0ae  34265  4atlem0be  34266  4atlem3b  34269  4atlem9  34274  4atlem10a  34275  4atlem10  34277  4atlem11a  34278  4atlem12a  34281  4at2  34285  2lplnm2N  34292  lneq2at  34449  2llnma1b  34457  2llnma1  34458  2llnma3r  34459  2llnma2  34460  2llnma2rN  34461  cdlema1N  34462  paddasslem2  34492  paddasslem16  34506  pmodlem1  34517  pmod2iN  34520  hlmod1i  34527  atmod2i1  34532  atmod2i2  34533  atmod3i1  34535  atmod3i2  34536  atmod4i1  34537  atmod4i2  34538  llnexchb2lem  34539  llnexch2N  34541  dalawlem3  34544  dalawlem4  34545  dalawlem5  34546  dalawlem6  34547  dalawlem7  34548  dalawlem8  34549  dalawlem9  34550  dalawlem11  34552  dalawlem12  34553  dalawlem13  34554  dalawlem15  34556  osumcllem7N  34633  osumcllem9N  34635  pl42lem1N  34650  4atexlemswapqr  34734  4atex2  34748  4atex2-0bOLDN  34750  trlval4  34859  cdlemc5  34866  cdlemc6  34867  cdlemd2  34870  cdlemd4  34872  cdlemd6  34874  cdleme00a  34880  cdleme0e  34888  cdleme4  34909  cdleme4a  34910  cdleme5  34911  cdleme9  34924  cdleme16aN  34930  cdleme11c  34932  cdleme11dN  34933  cdleme11e  34934  cdleme11g  34936  cdleme11h  34937  cdleme11j  34938  cdleme11k  34939  cdleme11l  34940  cdleme11  34941  cdleme12  34942  cdleme13  34943  cdleme14  34944  cdleme15a  34945  cdleme15c  34947  cdleme16b  34950  cdleme16c  34951  cdleme16d  34952  cdleme16e  34953  cdleme16f  34954  cdleme17d1  34960  cdleme0nex  34961  cdleme18a  34962  cdleme18b  34963  cdleme18c  34964  cdleme18d  34966  cdlemednpq  34970  cdlemednuN  34971  cdleme20zN  34972  cdleme20y  34973  cdleme19a  34974  cdleme19b  34975  cdleme19d  34977  cdleme19e  34978  cdleme20aN  34980  cdleme20d  34983  cdleme20f  34985  cdleme20g  34986  cdleme20i  34988  cdleme20j  34989  cdleme20l1  34991  cdleme20l2  34992  cdleme20l  34993  cdleme20m  34994  cdleme21b  34997  cdleme21c  34998  cdleme21e  35002  cdleme21j  35007  cdleme22aa  35010  cdleme22a  35011  cdleme22b  35012  cdleme22cN  35013  cdleme22d  35014  cdleme22e  35015  cdleme22eALTN  35016  cdleme22f  35017  cdleme26fALTN  35033  cdleme26f  35034  cdleme26f2ALTN  35035  cdleme26f2  35036  cdleme27N  35040  cdleme28a  35041  cdleme28b  35042  cdleme30a  35049  cdlemefs31fv1  35095  cdleme32b  35113  cdleme32c  35114  cdleme32e  35116  cdleme35h  35127  cdleme36a  35131  cdleme36m  35132  cdleme41sn3aw  35145  cdleme41sn4aw  35146  cdleme41fva11  35148  cdleme42k  35155  cdleme43cN  35162  cdleme46f2g1  35165  cdlemeg46fjgN  35192  cdlemeg46fjv  35194  cdlemeg46frv  35196  cdlemeg46rgv  35199  cdlemeg46req  35200  cdlemeg46gfv  35201  cdleme50trn2a  35221  cdlemg4a  35279  cdlemg4d  35284  cdlemg4e  35285  cdlemg4f  35286  cdlemg8c  35300  cdlemg9a  35303  cdlemg9b  35304  cdlemg10a  35311  cdlemg10  35312  cdlemg12b  35315  cdlemg12f  35319  cdlemg12g  35320  cdlemg12  35321  cdlemg17dN  35334  cdlemg17dALTN  35335  cdlemg17e  35336  cdlemg17f  35337  cdlemg17g  35338  cdlemg17i  35340  cdlemg17ir  35341  cdlemg17pq  35343  cdlemg17bq  35344  cdlemg17iqN  35345  cdlemg17  35348  cdlemg18b  35350  cdlemg18c  35351  cdlemg18d  35352  cdlemg18  35353  cdlemg19  35355  cdlemg21  35357  cdlemg28a  35364  cdlemg31b0a  35366  cdlemg27b  35367  cdlemg33b0  35372  cdlemg28b  35374  cdlemg28  35375  cdlemg35  35384  cdlemg36  35385  cdlemg44a  35402  cdlemh  35488  cdlemi2  35490  cdlemj1  35492  tendocan  35495  cdlemk5a  35506  cdlemk5  35507  cdlemki  35512  cdlemkvcl  35513  cdlemk10  35514  cdlemksv2  35518  cdlemk7  35519  cdlemk11  35520  cdlemk12  35521  cdlemkoatnle  35522  cdlemk15  35526  cdlemk16a  35527  cdlemk16  35528  cdlemk1u  35530  cdlemk5u  35532  cdlemk6u  35533  cdlemk18  35539  cdlemk19  35540  cdlemk7u  35541  cdlemk11u  35542  cdlemk12u  35543  cdlemk21N  35544  cdlemk20  35545  cdlemkoatnle-2N  35546  cdlemk13-2N  35547  cdlemkole-2N  35548  cdlemk14-2N  35549  cdlemk15-2N  35550  cdlemk16-2N  35551  cdlemk17-2N  35552  cdlemk18-2N  35557  cdlemk19-2N  35558  cdlemk22  35564  cdlemk30  35565  cdlemkuel-3  35569  cdlemkuv2-3N  35570  cdlemk18-3N  35571  cdlemkfid1N  35592  cdlemkid1  35593  cdlemkfid3N  35596  cdlemky  35597  cdlemk11ta  35600  cdlemk47  35620  cdlemk48  35621  cdlemk49  35622  cdlemk50  35623  cdlemk51  35624  cdlemk52  35625  cdlemk53a  35626  cdlemk53  35628  cdlemk54  35629  cdlemk55a  35630  cdlemkyyN  35633  cdlemk43N  35634  cdlemk55u1  35636  cdlemk55u  35637  cdlemk39u1  35638  cdlemk19u1  35640  cdleml1N  35647  cdleml2N  35648  cdleml3N  35649  dia2dimlem6  35741  cdlemn2  35867  cdlemn2a  35868  cdlemn5pre  35872  cdlemn11a  35879  dihjustlem  35888  dihjust  35889  dihmeetlem15N  35993  lclkrlem2y  36203
  Copyright terms: Public domain W3C validator