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

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

Proof of Theorem simp23
StepHypRef Expression
1 simp3 959 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl23  1037  simpr23  1046  simp123  1091  simp223  1100  simp323  1109  funtpg  5493  omeulem1  6817  elfiun  7427  cofsmo  8141  modexp  11506  iscatd2  13898  funcoppc  14064  funcres  14085  catcisolem  14253  1stfcl  14286  2ndfcl  14287  prfcl  14292  evlfcl  14311  curf1cl  14317  curfcl  14321  hofcl  14348  meetle  14449  prdsxmetlem  18390  isosctrlem3  20656  isosctr  20657  rhmdvd  24251  colinearalg  25841  ax5seglem6  25865  ax5seg  25869  axpasch  25872  axeuclid  25894  cgrtr  25918  cgrtr3  25920  ofscom  25933  btwnxfr  25982  colinearxfr  26001  lineext  26002  brofs2  26003  brifs2  26004  fscgr  26006  linecgr  26007  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem5  26017  btwnconn1lem6  26018  btwnconn1lem7  26019  seglecgr12im  26036  seglecgr12  26037  segletr  26040  broutsideof3  26052  outsideofeq  26056  lineunray  26073  bnj966  29252  bnj967  29253  eqlkr  29834  omlmod1i2N  29995  cvrcmp2  30019  cvlexch2  30064  cvlexchb2  30066  cvlatexchb2  30070  cvlatexch1  30071  cvlatexch2  30072  cvlatexch3  30073  cvlsupr7  30083  cvlsupr8  30084  atnlej1  30113  atnlej2  30114  2llnneN  30143  cvratlem  30155  atcvrneN  30164  atcvrj1  30165  atlelt  30172  2atjm  30179  3noncolr2  30183  3noncolr1N  30184  hlatcon2  30186  3dimlem2  30193  3dim1  30201  3dim2  30202  1cvrat  30210  ps-1  30211  ps-2  30212  2atjlej  30213  hlatexch3N  30214  ps-2b  30216  3atlem1  30217  3atlem2  30218  3atlem6  30222  llnle  30252  2atm  30261  ps-2c  30262  lplni2  30271  lplnle  30274  lplnnle2at  30275  lplnri3N  30289  llncvrlpln2  30291  2atmat  30295  2llnjaN  30300  2llnm2N  30302  2llnm4  30304  2llnmeqat  30305  lvolnle3at  30316  4atlem0ae  30328  4atlem0be  30329  4atlem3b  30332  4atlem9  30337  4atlem10a  30338  4atlem10  30340  4atlem11a  30341  4atlem12a  30344  4at  30347  4at2  30348  lplncvrlvol2  30349  2lplnm2N  30355  2llnma1b  30520  2llnma1  30521  2llnma3r  30522  2llnma2  30523  2llnma2rN  30524  cdlema1N  30525  cdlema2N  30526  paddasslem2  30555  paddasslem15  30568  paddasslem16  30569  pmodlem1  30580  pmod2iN  30583  hlmod1i  30590  atmod2i1  30595  atmod2i2  30596  atmod3i1  30598  atmod3i2  30599  atmod4i1  30600  atmod4i2  30601  llnexchb2  30603  dalawlem3  30607  dalawlem4  30608  dalawlem5  30609  dalawlem6  30610  dalawlem7  30611  dalawlem8  30612  dalawlem9  30613  dalawlem11  30615  dalawlem13  30617  dalawlem15  30619  osumcllem7N  30696  osumcllem9N  30698  osumcllem11N  30700  pl42lem1N  30713  4atex  30810  4atex2-0aOLDN  30812  4atex2-0bOLDN  30813  4atex2-0cOLDN  30814  trlval4  30922  cdlemc5  30929  cdlemd5  30936  cdlemd6  30937  cdleme00a  30943  cdleme3g  30968  cdleme3h  30969  cdleme3  30971  cdleme4  30972  cdleme4a  30973  cdleme16aN  30993  cdleme11c  30995  cdleme11g  30999  cdleme11h  31000  cdleme12  31005  cdleme0nex  31024  cdleme18a  31025  cdleme18b  31026  cdleme18c  31027  cdleme18d  31029  cdleme20zN  31035  cdleme20y  31036  cdleme19a  31037  cdleme19b  31038  cdleme19d  31040  cdleme19e  31041  cdleme20aN  31043  cdleme20c  31045  cdleme20d  31046  cdleme20i  31051  cdleme20j  31052  cdleme20l1  31054  cdleme20l2  31055  cdleme20m  31057  cdleme21b  31060  cdleme21c  31061  cdleme21j  31070  cdleme22aa  31073  cdleme22a  31074  cdleme22eALTN  31079  cdleme26e  31093  cdleme26fALTN  31096  cdleme26f  31097  cdleme26f2ALTN  31098  cdleme26f2  31099  cdleme27N  31103  cdleme28a  31104  cdleme28b  31105  cdleme30a  31112  cdlemefs45eN  31165  cdleme32c  31177  cdleme32e  31179  cdleme35h  31190  cdleme36a  31194  cdleme36m  31195  cdleme37m  31196  cdleme41sn3aw  31208  cdleme41sn4aw  31209  cdleme41fva11  31211  cdleme42k  31218  cdleme43cN  31225  cdleme43dN  31226  cdleme46f2g1  31228  cdlemeg47rv2  31244  cdlemeg46sfg  31254  cdlemeg46fjgN  31255  cdlemeg46rjgN  31256  cdlemeg46fjv  31257  cdlemeg46frv  31259  cdlemeg46vrg  31261  cdlemeg46rgv  31262  cdlemeg46req  31263  cdlemeg46gfv  31264  cdleme50trn2a  31284  cdlemg2fv2  31334  cdlemg4a  31342  cdlemg4e  31348  cdlemg4f  31349  cdlemg8b  31362  cdlemg8c  31363  cdlemg9a  31366  cdlemg9b  31367  cdlemg9  31368  cdlemg10a  31374  cdlemg12a  31377  cdlemg12b  31378  cdlemg12c  31379  cdlemg12  31384  cdlemg17dN  31397  cdlemg17dALTN  31398  cdlemg17e  31399  cdlemg17i  31403  cdlemg17ir  31404  cdlemg17pq  31406  cdlemg17bq  31407  cdlemg17iqN  31408  cdlemg17  31411  cdlemg18b  31413  cdlemg18c  31414  cdlemg18d  31415  cdlemg18  31416  cdlemg19  31418  cdlemg21  31420  cdlemg28a  31427  cdlemg31b0a  31429  cdlemg33b0  31435  cdlemg35  31447  cdlemg44a  31465  cdlemh  31551  cdlemi2  31553  cdlemj1  31555  cdlemk5a  31569  cdlemk5  31570  cdlemki  31575  cdlemkvcl  31576  cdlemk10  31577  cdlemksv2  31581  cdlemk7  31582  cdlemk11  31583  cdlemk12  31584  cdlemk15  31589  cdlemk16a  31590  cdlemk16  31591  cdlemk5u  31595  cdlemk6u  31596  cdlemk18  31602  cdlemk19  31603  cdlemk7u  31604  cdlemk11u  31605  cdlemk12u  31606  cdlemk21N  31607  cdlemk20  31608  cdlemkoatnle-2N  31609  cdlemk13-2N  31610  cdlemkole-2N  31611  cdlemk14-2N  31612  cdlemk15-2N  31613  cdlemk16-2N  31614  cdlemk17-2N  31615  cdlemk18-2N  31620  cdlemk19-2N  31621  cdlemk22  31627  cdlemk30  31628  cdlemk28-3  31642  cdlemk33N  31643  cdlemkfid1N  31655  cdlemkid1  31656  cdlemky  31660  cdlemk11ta  31663  cdlemk35s-id  31672  cdlemk39s-id  31674  cdlemk47  31683  cdlemk48  31684  cdlemk49  31685  cdlemk50  31686  cdlemk51  31687  cdlemk52  31688  cdlemk53a  31689  cdlemk53b  31690  cdlemk53  31691  cdlemk54  31692  cdlemk55a  31693  cdlemkyyN  31696  cdlemk43N  31697  cdlemk55u1  31699  cdlemk55u  31700  cdlemk39u1  31701  cdlemk19u1  31703  cdleml1N  31710  cdleml2N  31711  cdleml3N  31712  dia2dimlem6  31804  cdlemn2  31930  cdlemn2a  31931  cdlemn5pre  31935  cdlemn11pre  31945  dihjustlem  31951  dihjust  31952  dihmeetlem15N  32056  lclkrlem2y  32266
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