Theorem simp21 1030

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 997	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
2	1	3ad2ant2 1019	1 |- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ w3a 974

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 976

This theorem is referenced by:  simpl21  1075  simpr21  1084  simp121  1129  simp221  1138  simp321  1147  omeulem1  7268  cofsmo  8681  axdc4lem  8867  0catg  15301  funcoppc  15488  funcres  15509  catcisolem  15709  1stfcl  15790  2ndfcl  15791  prfcl  15796  evlfcl  15815  curf1cl  15821  curfcl  15825  hofcl  15852  mulgdirlem  16490  mdetunilem4  19409  mdetuni0  19415  mdetmul  19417  prdsxmetlem  21163  isosctrlem3  23479  isosctr  23480  amgmlem  23645  f1otrg  24591  colinearalg  24630  ax5seglem6  24654  ax5seg  24658  axpasch  24661  axeuclidlem  24682  axeuclid  24683  ogrpsub  28159  ogrpaddlt  28160  ogrpsublt  28164  rhmdvd  28264  bnj1128  29373  mclspps  29796  cgrtr  30330  cgrtr3  30332  ofscom  30345  segconeq  30348  ifscgr  30382  btwnxfr  30394  colinearxfr  30413  lineext  30414  brofs2  30415  brifs2  30416  fscgr  30418  linecgr  30419  btwnconn1lem1  30425  btwnconn1lem2  30426  btwnconn1lem3  30427  btwnconn1lem4  30428  btwnconn1lem5  30429  btwnconn1lem6  30430  btwnconn1lem7  30431  seglecgr12im  30448  seglecgr12  30449  segletr  30452  broutsideof3  30464  outsideofeq  30468  lineunray  30485  lineelsb2  30486  linecom  30488  lshpkrlem5  32132  omlmod1i2N  32278  cvrnbtwn3  32294  cvrcmp  32301  cvrcmp2  32302  cvlexch2  32347  cvlexchb2  32349  cvlatexchb2  32353  cvlatexch2  32355  cvlatexch3  32356  cvlsupr7  32366  atnlej1  32396  atnlej2  32397  2llnneN  32426  cvratlem  32438  atcvrneN  32447  atcvrj1  32448  atlelt  32455  2atjm  32462  3noncolr2  32466  3noncolr1N  32467  3dimlem2  32476  3dim1  32484  3dim2  32485  1cvrat  32493  ps-1  32494  ps-2  32495  2atjlej  32496  hlatexch3N  32497  ps-2b  32499  3atlem1  32500  3atlem2  32501  3atlem5  32504  3atlem6  32505  llnle  32535  2atm  32544  ps-2c  32545  lplni2  32554  lplnle  32557  lplnnle2at  32558  lplnri3N  32572  llncvrlpln2  32574  2atmat  32578  2llnm2N  32585  2llnm4  32587  2llnmeqat  32588  lvolnle3at  32599  4atlem0ae  32611  4atlem0be  32612  4atlem3b  32615  4atlem9  32620  4atlem10a  32621  4atlem10  32623  4atlem11a  32624  4atlem12a  32627  4at2  32631  2lplnm2N  32638  lneq2at  32795  2llnma1b  32803  2llnma1  32804  2llnma3r  32805  2llnma2  32806  2llnma2rN  32807  cdlema1N  32808  paddasslem2  32838  paddasslem15  32851  paddasslem16  32852  pmodlem1  32863  pmodlem2  32864  pmod2iN  32866  hlmod1i  32873  atmod1i1m  32875  atmod2i1  32878  atmod2i2  32879  atmod3i1  32881  atmod3i2  32882  atmod4i1  32883  atmod4i2  32884  llnexchb2lem  32885  llnexch2N  32887  dalawlem3  32890  dalawlem4  32891  dalawlem5  32892  dalawlem6  32893  dalawlem7  32894  dalawlem8  32895  dalawlem9  32896  dalawlem11  32898  dalawlem12  32899  dalawlem13  32900  dalawlem15  32902  osumcllem9N  32981  pl42lem1N  32996  4atexlems  33069  4atex2  33094  4atex2-0bOLDN  33096  trlval4  33206  cdlemc5  33213  cdlemc6  33214  cdlemd2  33217  cdlemd4  33219  cdlemd6  33221  cdleme00a  33227  cdleme0e  33235  cdleme3g  33252  cdleme3h  33253  cdleme3  33255  cdleme4  33256  cdleme4a  33257  cdleme5  33258  cdleme9  33271  cdleme16aN  33277  cdleme11c  33279  cdleme11e  33281  cdleme11g  33283  cdleme11h  33284  cdleme11j  33285  cdleme11k  33286  cdleme11l  33287  cdleme11  33288  cdleme12  33289  cdleme14  33291  cdleme15c  33294  cdleme16b  33297  cdleme16c  33298  cdleme16d  33299  cdleme16e  33300  cdleme16f  33301  cdleme0nex  33308  cdleme18a  33309  cdleme18c  33311  cdleme18d  33313  cdlemednpq  33317  cdlemednuN  33318  cdleme20zN  33319  cdleme20y  33320  cdleme20yOLD  33321  cdleme19a  33322  cdleme19b  33323  cdleme19d  33325  cdleme19e  33326  cdleme20aN  33328  cdleme20bN  33329  cdleme20c  33330  cdleme20d  33331  cdleme20f  33333  cdleme20g  33334  cdleme20i  33336  cdleme20j  33337  cdleme20l1  33339  cdleme20l2  33340  cdleme20l  33341  cdleme20m  33342  cdleme21b  33345  cdleme21c  33346  cdleme21e  33350  cdleme21f  33351  cdleme22a  33359  cdleme22b  33360  cdleme22e  33363  cdleme22eALTN  33364  cdleme22f  33365  cdleme26eALTN  33380  cdleme26fALTN  33381  cdleme26f  33382  cdleme26f2ALTN  33383  cdleme26f2  33384  cdleme27N  33388  cdleme28a  33389  cdleme28b  33390  cdleme30a  33397  cdleme43fsv1snlem  33439  cdlemefs31fv1  33443  cdlemefs45eN  33450  cdleme32b  33461  cdleme32c  33462  cdleme32d  33463  cdleme35h  33475  cdleme36a  33479  cdleme36m  33480  cdleme37m  33481  cdleme40m  33486  cdleme40n  33487  cdleme41sn3aw  33493  cdleme41sn4aw  33494  cdleme41fva11  33496  cdleme42k  33503  cdleme43cN  33510  cdleme43dN  33511  cdleme46f2g1  33513  cdlemeg47rv2  33529  cdlemeg46sfg  33539  cdlemeg46fjgN  33540  cdlemeg46rjgN  33541  cdlemeg46fjv  33542  cdlemeg46frv  33544  cdlemeg46vrg  33546  cdlemeg46rgv  33547  cdlemeg46req  33548  cdlemeg46gfv  33549  cdlemg4a  33627  cdlemg4d  33632  cdlemg4e  33633  cdlemg4f  33634  cdlemg4g  33635  cdlemg4  33636  cdlemg6d  33640  cdlemg6e  33641  cdlemg8b  33647  cdlemg8c  33648  cdlemg9a  33651  cdlemg9b  33652  cdlemg10a  33659  cdlemg10  33660  cdlemg12a  33662  cdlemg12b  33663  cdlemg12f  33667  cdlemg12g  33668  cdlemg12  33669  cdlemg17dN  33682  cdlemg17dALTN  33683  cdlemg17e  33684  cdlemg17f  33685  cdlemg17g  33686  cdlemg17h  33687  cdlemg17i  33688  cdlemg17pq  33691  cdlemg17iqN  33693  cdlemg17  33696  cdlemg18b  33698  cdlemg18c  33699  cdlemg19a  33702  cdlemg19  33703  cdlemg28a  33712  cdlemg27b  33715  cdlemg28b  33722  cdlemg28  33723  cdlemg33a  33725  cdlemg33b  33726  cdlemg33c  33727  cdlemg33d  33728  cdlemg33e  33729  cdlemg33  33730  cdlemg35  33732  cdlemg36  33733  cdlemg44a  33750  cdlemh  33836  cdlemi2  33838  cdlemj1  33840  tendocan  33843  cdlemk5a  33854  cdlemki  33860  cdlemkvcl  33861  cdlemk10  33862  cdlemksv2  33866  cdlemkole  33872  cdlemk14  33873  cdlemk15  33874  cdlemk16a  33875  cdlemk16  33876  cdlemk17  33877  cdlemk18  33887  cdlemk19  33888  cdlemkoatnle-2N  33894  cdlemk13-2N  33895  cdlemkole-2N  33896  cdlemk14-2N  33897  cdlemk15-2N  33898  cdlemk16-2N  33899  cdlemk17-2N  33900  cdlemk18-2N  33905  cdlemk19-2N  33906  cdlemk30  33913  cdlemk18-3N  33919  cdlemk23-3  33921  cdlemk25-3  33923  cdlemk27-3  33926  cdlemk37  33933  cdlemkfid1N  33940  cdlemkid1  33941  cdlemky  33945  cdlemk11ta  33948  cdlemk47  33968  cdlemk48  33969  cdlemk49  33970  cdlemk50  33971  cdlemk51  33972  cdlemk52  33973  cdlemk53a  33974  cdlemk54  33977  cdlemk39u1  33986  cdlemk19u1  33988  cdleml1N  33995  cdleml2N  33996  cdleml3N  33997  dia2dimlem6  34089  cdlemn2  34215  cdlemn2a  34216  cdlemn5pre  34220  cdlemn10  34226  cdlemn11c  34229  cdlemn11pre  34230  dihjustlem  34236  dihjust  34237  lclkrlem2y  34551  relexpmulnn  35688  lincreslvec3  38594