Theorem simp21 1041

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp21	|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ps )

Proof of Theorem simp21

Step	Hyp	Ref	Expression
1		simp1 1008	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
2	1	3ad2ant2 1030	1 |- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ w3a 985

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 987

This theorem is referenced by:  simpl21  1086  simpr21  1095  simp121  1140  simp221  1149  simp321  1158  omeulem1  7283  cofsmo  8699  axdc4lem  8885  0catg  15593  funcoppc  15780  funcres  15801  catcisolem  16001  1stfcl  16082  2ndfcl  16083  prfcl  16088  evlfcl  16107  curf1cl  16113  curfcl  16117  hofcl  16144  mulgdirlem  16782  mdetunilem4  19640  mdetuni0  19646  mdetmul  19648  prdsxmetlem  21383  isosctrlem3  23749  isosctr  23750  amgmlem  23915  f1otrg  24901  colinearalg  24940  ax5seglem6  24964  ax5seg  24968  axpasch  24971  axeuclidlem  24992  axeuclid  24993  ogrpsub  28480  ogrpaddlt  28481  ogrpsublt  28485  rhmdvd  28584  bnj1128  29799  mclspps  30222  cgrtr  30759  cgrtr3  30761  ofscom  30774  segconeq  30777  ifscgr  30811  btwnxfr  30823  colinearxfr  30842  lineext  30843  brofs2  30844  brifs2  30845  fscgr  30847  linecgr  30848  btwnconn1lem1  30854  btwnconn1lem2  30855  btwnconn1lem3  30856  btwnconn1lem4  30857  btwnconn1lem5  30858  btwnconn1lem6  30859  btwnconn1lem7  30860  seglecgr12im  30877  seglecgr12  30878  segletr  30881  broutsideof3  30893  outsideofeq  30897  lineunray  30914  lineelsb2  30915  linecom  30917  lshpkrlem5  32680  omlmod1i2N  32826  cvrnbtwn3  32842  cvrcmp  32849  cvrcmp2  32850  cvlexch2  32895  cvlexchb2  32897  cvlatexchb2  32901  cvlatexch2  32903  cvlatexch3  32904  cvlsupr7  32914  atnlej1  32944  atnlej2  32945  2llnneN  32974  cvratlem  32986  atcvrneN  32995  atcvrj1  32996  atlelt  33003  2atjm  33010  3noncolr2  33014  3noncolr1N  33015  3dimlem2  33024  3dim1  33032  3dim2  33033  1cvrat  33041  ps-1  33042  ps-2  33043  2atjlej  33044  hlatexch3N  33045  ps-2b  33047  3atlem1  33048  3atlem2  33049  3atlem5  33052  3atlem6  33053  llnle  33083  2atm  33092  ps-2c  33093  lplni2  33102  lplnle  33105  lplnnle2at  33106  lplnri3N  33120  llncvrlpln2  33122  2atmat  33126  2llnm2N  33133  2llnm4  33135  2llnmeqat  33136  lvolnle3at  33147  4atlem0ae  33159  4atlem0be  33160  4atlem3b  33163  4atlem9  33168  4atlem10a  33169  4atlem10  33171  4atlem11a  33172  4atlem12a  33175  4at2  33179  2lplnm2N  33186  lneq2at  33343  2llnma1b  33351  2llnma1  33352  2llnma3r  33353  2llnma2  33354  2llnma2rN  33355  cdlema1N  33356  paddasslem2  33386  paddasslem15  33399  paddasslem16  33400  pmodlem1  33411  pmodlem2  33412  pmod2iN  33414  hlmod1i  33421  atmod1i1m  33423  atmod2i1  33426  atmod2i2  33427  atmod3i1  33429  atmod3i2  33430  atmod4i1  33431  atmod4i2  33432  llnexchb2lem  33433  llnexch2N  33435  dalawlem3  33438  dalawlem4  33439  dalawlem5  33440  dalawlem6  33441  dalawlem7  33442  dalawlem8  33443  dalawlem9  33444  dalawlem11  33446  dalawlem12  33447  dalawlem13  33448  dalawlem15  33450  osumcllem9N  33529  pl42lem1N  33544  4atexlems  33617  4atex2  33642  4atex2-0bOLDN  33644  trlval4  33754  cdlemc5  33761  cdlemc6  33762  cdlemd2  33765  cdlemd4  33767  cdlemd6  33769  cdleme00a  33775  cdleme0e  33783  cdleme3g  33800  cdleme3h  33801  cdleme3  33803  cdleme4  33804  cdleme4a  33805  cdleme5  33806  cdleme9  33819  cdleme16aN  33825  cdleme11c  33827  cdleme11e  33829  cdleme11g  33831  cdleme11h  33832  cdleme11j  33833  cdleme11k  33834  cdleme11l  33835  cdleme11  33836  cdleme12  33837  cdleme14  33839  cdleme15c  33842  cdleme16b  33845  cdleme16c  33846  cdleme16d  33847  cdleme16e  33848  cdleme16f  33849  cdleme0nex  33856  cdleme18a  33857  cdleme18c  33859  cdleme18d  33861  cdlemednpq  33865  cdlemednuN  33866  cdleme20zN  33867  cdleme20y  33868  cdleme20yOLD  33869  cdleme19a  33870  cdleme19b  33871  cdleme19d  33873  cdleme19e  33874  cdleme20aN  33876  cdleme20bN  33877  cdleme20c  33878  cdleme20d  33879  cdleme20f  33881  cdleme20g  33882  cdleme20i  33884  cdleme20j  33885  cdleme20l1  33887  cdleme20l2  33888  cdleme20l  33889  cdleme20m  33890  cdleme21b  33893  cdleme21c  33894  cdleme21e  33898  cdleme21f  33899  cdleme22a  33907  cdleme22b  33908  cdleme22e  33911  cdleme22eALTN  33912  cdleme22f  33913  cdleme26eALTN  33928  cdleme26fALTN  33929  cdleme26f  33930  cdleme26f2ALTN  33931  cdleme26f2  33932  cdleme27N  33936  cdleme28a  33937  cdleme28b  33938  cdleme30a  33945  cdleme43fsv1snlem  33987  cdlemefs31fv1  33991  cdlemefs45eN  33998  cdleme32b  34009  cdleme32c  34010  cdleme32d  34011  cdleme35h  34023  cdleme36a  34027  cdleme36m  34028  cdleme37m  34029  cdleme40m  34034  cdleme40n  34035  cdleme41sn3aw  34041  cdleme41sn4aw  34042  cdleme41fva11  34044  cdleme42k  34051  cdleme43cN  34058  cdleme43dN  34059  cdleme46f2g1  34061  cdlemeg47rv2  34077  cdlemeg46sfg  34087  cdlemeg46fjgN  34088  cdlemeg46rjgN  34089  cdlemeg46fjv  34090  cdlemeg46frv  34092  cdlemeg46vrg  34094  cdlemeg46rgv  34095  cdlemeg46req  34096  cdlemeg46gfv  34097  cdlemg4a  34175  cdlemg4d  34180  cdlemg4e  34181  cdlemg4f  34182  cdlemg4g  34183  cdlemg4  34184  cdlemg6d  34188  cdlemg6e  34189  cdlemg8b  34195  cdlemg8c  34196  cdlemg9a  34199  cdlemg9b  34200  cdlemg10a  34207  cdlemg10  34208  cdlemg12a  34210  cdlemg12b  34211  cdlemg12f  34215  cdlemg12g  34216  cdlemg12  34217  cdlemg17dN  34230  cdlemg17dALTN  34231  cdlemg17e  34232  cdlemg17f  34233  cdlemg17g  34234  cdlemg17h  34235  cdlemg17i  34236  cdlemg17pq  34239  cdlemg17iqN  34241  cdlemg17  34244  cdlemg18b  34246  cdlemg18c  34247  cdlemg19a  34250  cdlemg19  34251  cdlemg28a  34260  cdlemg27b  34263  cdlemg28b  34270  cdlemg28  34271  cdlemg33a  34273  cdlemg33b  34274  cdlemg33c  34275  cdlemg33d  34276  cdlemg33e  34277  cdlemg33  34278  cdlemg35  34280  cdlemg36  34281  cdlemg44a  34298  cdlemh  34384  cdlemi2  34386  cdlemj1  34388  tendocan  34391  cdlemk5a  34402  cdlemki  34408  cdlemkvcl  34409  cdlemk10  34410  cdlemksv2  34414  cdlemkole  34420  cdlemk14  34421  cdlemk15  34422  cdlemk16a  34423  cdlemk16  34424  cdlemk17  34425  cdlemk18  34435  cdlemk19  34436  cdlemkoatnle-2N  34442  cdlemk13-2N  34443  cdlemkole-2N  34444  cdlemk14-2N  34445  cdlemk15-2N  34446  cdlemk16-2N  34447  cdlemk17-2N  34448  cdlemk18-2N  34453  cdlemk19-2N  34454  cdlemk30  34461  cdlemk18-3N  34467  cdlemk23-3  34469  cdlemk25-3  34471  cdlemk27-3  34474  cdlemk37  34481  cdlemkfid1N  34488  cdlemkid1  34489  cdlemky  34493  cdlemk11ta  34496  cdlemk47  34516  cdlemk48  34517  cdlemk49  34518  cdlemk50  34519  cdlemk51  34520  cdlemk52  34521  cdlemk53a  34522  cdlemk54  34525  cdlemk39u1  34534  cdlemk19u1  34536  cdleml1N  34543  cdleml2N  34544  cdleml3N  34545  dia2dimlem6  34637  cdlemn2  34763  cdlemn2a  34764  cdlemn5pre  34768  cdlemn10  34774  cdlemn11c  34777  cdlemn11pre  34778  dihjustlem  34784  dihjust  34785  lclkrlem2y  35099  relexpmulnn  36301  lincreslvec3  40328