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

Theorem simp23 1029
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 996 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 1016 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simpl23  1074  simpr23  1083  simp123  1128  simp223  1137  simp323  1146  funtpg  5620  omeulem1  7223  elfiun  7882  cofsmo  8640  modexp  12286  iscatd2  15173  funcoppc  15366  funcres  15387  catcisolem  15587  1stfcl  15668  2ndfcl  15669  prfcl  15674  evlfcl  15693  curf1cl  15699  curfcl  15703  hofcl  15730  pmtrprfv3  16681  mdetunilem3  19286  mdetunilem4  19287  mdetuni0  19293  mdetmul  19295  prdsxmetlem  21040  isosctrlem3  23354  isosctr  23355  f1otrg  24379  colinearalg  24418  ax5seglem6  24442  ax5seg  24446  axpasch  24449  axeuclid  24471  ogrpsub  27944  ogrpsublt  27949  rhmdvd  28049  mclspps  29211  cgrtr  29873  cgrtr3  29875  ofscom  29888  btwnxfr  29937  colinearxfr  29956  lineext  29957  brofs2  29958  brifs2  29959  fscgr  29961  linecgr  29962  btwnconn1lem1  29968  btwnconn1lem2  29969  btwnconn1lem3  29970  btwnconn1lem4  29971  btwnconn1lem5  29972  btwnconn1lem6  29973  btwnconn1lem7  29974  seglecgr12im  29991  seglecgr12  29992  segletr  29995  broutsideof3  30007  outsideofeq  30011  lineunray  30028  bnj966  34422  bnj967  34423  eqlkr  35240  omlmod1i2N  35401  cvrcmp2  35425  cvlexch2  35470  cvlexchb2  35472  cvlatexchb2  35476  cvlatexch1  35477  cvlatexch2  35478  cvlatexch3  35479  cvlsupr7  35489  cvlsupr8  35490  atnlej1  35519  atnlej2  35520  2llnneN  35549  cvratlem  35561  atcvrneN  35570  atcvrj1  35571  atlelt  35578  2atjm  35585  3noncolr2  35589  3noncolr1N  35590  hlatcon2  35592  3dimlem2  35599  3dim1  35607  3dim2  35608  1cvrat  35616  ps-1  35617  ps-2  35618  2atjlej  35619  hlatexch3N  35620  ps-2b  35622  3atlem1  35623  3atlem2  35624  3atlem6  35628  llnle  35658  2atm  35667  ps-2c  35668  lplni2  35677  lplnle  35680  lplnnle2at  35681  lplnri3N  35695  llncvrlpln2  35697  2atmat  35701  2llnjaN  35706  2llnm2N  35708  2llnm4  35710  2llnmeqat  35711  lvolnle3at  35722  4atlem0ae  35734  4atlem0be  35735  4atlem3b  35738  4atlem9  35743  4atlem10a  35744  4atlem10  35746  4atlem11a  35747  4atlem12a  35750  4at  35753  4at2  35754  lplncvrlvol2  35755  2lplnm2N  35761  2llnma1b  35926  2llnma1  35927  2llnma3r  35928  2llnma2  35929  2llnma2rN  35930  cdlema1N  35931  cdlema2N  35932  paddasslem2  35961  paddasslem15  35974  paddasslem16  35975  pmodlem1  35986  pmod2iN  35989  hlmod1i  35996  atmod2i1  36001  atmod2i2  36002  atmod3i1  36004  atmod3i2  36005  atmod4i1  36006  atmod4i2  36007  llnexchb2  36009  dalawlem3  36013  dalawlem4  36014  dalawlem5  36015  dalawlem6  36016  dalawlem7  36017  dalawlem8  36018  dalawlem9  36019  dalawlem11  36021  dalawlem13  36023  dalawlem15  36025  osumcllem7N  36102  osumcllem9N  36104  osumcllem11N  36106  pl42lem1N  36119  4atex  36216  4atex2-0aOLDN  36218  4atex2-0bOLDN  36219  4atex2-0cOLDN  36220  trlval4  36329  cdlemc5  36336  cdlemd5  36343  cdlemd6  36344  cdleme00a  36350  cdleme3g  36375  cdleme3h  36376  cdleme3  36378  cdleme4  36379  cdleme4a  36380  cdleme16aN  36400  cdleme11c  36402  cdleme11g  36406  cdleme11h  36407  cdleme12  36412  cdleme0nex  36431  cdleme18a  36432  cdleme18b  36433  cdleme18c  36434  cdleme18d  36436  cdleme20zN  36442  cdleme20y  36443  cdleme20yOLD  36444  cdleme19a  36445  cdleme19b  36446  cdleme19d  36448  cdleme19e  36449  cdleme20aN  36451  cdleme20c  36453  cdleme20d  36454  cdleme20i  36459  cdleme20j  36460  cdleme20l1  36462  cdleme20l2  36463  cdleme20m  36465  cdleme21b  36468  cdleme21c  36469  cdleme21j  36478  cdleme22aa  36481  cdleme22a  36482  cdleme22eALTN  36487  cdleme26e  36501  cdleme26fALTN  36504  cdleme26f  36505  cdleme26f2ALTN  36506  cdleme26f2  36507  cdleme27N  36511  cdleme28a  36512  cdleme28b  36513  cdleme30a  36520  cdlemefs45eN  36573  cdleme32c  36585  cdleme32e  36587  cdleme35h  36598  cdleme36a  36602  cdleme36m  36603  cdleme37m  36604  cdleme41sn3aw  36616  cdleme41sn4aw  36617  cdleme41fva11  36619  cdleme42k  36626  cdleme43cN  36633  cdleme43dN  36634  cdleme46f2g1  36636  cdlemeg47rv2  36652  cdlemeg46sfg  36662  cdlemeg46fjgN  36663  cdlemeg46rjgN  36664  cdlemeg46fjv  36665  cdlemeg46frv  36667  cdlemeg46vrg  36669  cdlemeg46rgv  36670  cdlemeg46req  36671  cdlemeg46gfv  36672  cdleme50trn2a  36692  cdlemg2fv2  36742  cdlemg4a  36750  cdlemg4e  36756  cdlemg4f  36757  cdlemg8b  36770  cdlemg8c  36771  cdlemg9a  36774  cdlemg9b  36775  cdlemg9  36776  cdlemg10a  36782  cdlemg12a  36785  cdlemg12b  36786  cdlemg12c  36787  cdlemg12  36792  cdlemg17dN  36805  cdlemg17dALTN  36806  cdlemg17e  36807  cdlemg17i  36811  cdlemg17ir  36812  cdlemg17pq  36814  cdlemg17bq  36815  cdlemg17iqN  36816  cdlemg17  36819  cdlemg18b  36821  cdlemg18c  36822  cdlemg18d  36823  cdlemg18  36824  cdlemg19  36826  cdlemg21  36828  cdlemg28a  36835  cdlemg31b0a  36837  cdlemg33b0  36843  cdlemg35  36855  cdlemg44a  36873  cdlemh  36959  cdlemi2  36961  cdlemj1  36963  cdlemk5a  36977  cdlemk5  36978  cdlemki  36983  cdlemkvcl  36984  cdlemk10  36985  cdlemksv2  36989  cdlemk7  36990  cdlemk11  36991  cdlemk12  36992  cdlemk15  36997  cdlemk16a  36998  cdlemk16  36999  cdlemk5u  37003  cdlemk6u  37004  cdlemk18  37010  cdlemk19  37011  cdlemk7u  37012  cdlemk11u  37013  cdlemk12u  37014  cdlemk21N  37015  cdlemk20  37016  cdlemkoatnle-2N  37017  cdlemk13-2N  37018  cdlemkole-2N  37019  cdlemk14-2N  37020  cdlemk15-2N  37021  cdlemk16-2N  37022  cdlemk17-2N  37023  cdlemk18-2N  37028  cdlemk19-2N  37029  cdlemk22  37035  cdlemk30  37036  cdlemk28-3  37050  cdlemk33N  37051  cdlemkfid1N  37063  cdlemkid1  37064  cdlemky  37068  cdlemk11ta  37071  cdlemk35s-id  37080  cdlemk39s-id  37082  cdlemk47  37091  cdlemk48  37092  cdlemk49  37093  cdlemk50  37094  cdlemk51  37095  cdlemk52  37096  cdlemk53a  37097  cdlemk53b  37098  cdlemk53  37099  cdlemk54  37100  cdlemk55a  37101  cdlemkyyN  37104  cdlemk43N  37105  cdlemk55u1  37107  cdlemk55u  37108  cdlemk39u1  37109  cdlemk19u1  37111  cdleml1N  37118  cdleml2N  37119  cdleml3N  37120  dia2dimlem6  37212  cdlemn2  37338  cdlemn2a  37339  cdlemn5pre  37343  cdlemn11pre  37353  dihjustlem  37359  dihjust  37360  dihmeetlem15N  37464  lclkrlem2y  37674  relexpxpnnidm  38246
  Copyright terms: Public domain W3C validator