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 371  df-3an 976

This theorem is referenced by:  simpl21  1075  simpr21  1084  simp121  1129  simp221  1138  simp321  1147  omeulem1  7233  cofsmo  8652  axdc4lem  8838  0catg  14961  funcoppc  15118  funcres  15139  catcisolem  15307  1stfcl  15340  2ndfcl  15341  prfcl  15346  evlfcl  15365  curf1cl  15371  curfcl  15375  hofcl  15402  mulgdirlem  16040  mdetunilem4  18990  mdetuni0  18996  mdetmul  18998  prdsxmetlem  20744  isosctrlem3  23026  isosctr  23027  amgmlem  23191  f1otrg  24046  colinearalg  24085  ax5seglem6  24109  ax5seg  24113  axpasch  24116  axeuclidlem  24137  axeuclid  24138  ogrpsub  27580  ogrpaddlt  27581  ogrpsublt  27585  rhmdvd  27684  mclspps  28817  cgrtr  29617  cgrtr3  29619  ofscom  29632  segconeq  29635  ifscgr  29669  btwnxfr  29681  colinearxfr  29700  lineext  29701  brofs2  29702  brifs2  29703  fscgr  29705  linecgr  29706  btwnconn1lem1  29712  btwnconn1lem2  29713  btwnconn1lem3  29714  btwnconn1lem4  29715  btwnconn1lem5  29716  btwnconn1lem6  29717  btwnconn1lem7  29718  seglecgr12im  29735  seglecgr12  29736  segletr  29739  broutsideof3  29751  outsideofeq  29755  lineunray  29772  lineelsb2  29773  linecom  29775  lincreslvec3  32813  bnj1128  33774  lshpkrlem5  34573  omlmod1i2N  34719  cvrnbtwn3  34735  cvrcmp  34742  cvrcmp2  34743  cvlexch2  34788  cvlexchb2  34790  cvlatexchb2  34794  cvlatexch2  34796  cvlatexch3  34797  cvlsupr7  34807  atnlej1  34837  atnlej2  34838  2llnneN  34867  cvratlem  34879  atcvrneN  34888  atcvrj1  34889  atlelt  34896  2atjm  34903  3noncolr2  34907  3noncolr1N  34908  3dimlem2  34917  3dim1  34925  3dim2  34926  1cvrat  34934  ps-1  34935  ps-2  34936  2atjlej  34937  hlatexch3N  34938  ps-2b  34940  3atlem1  34941  3atlem2  34942  3atlem5  34945  3atlem6  34946  llnle  34976  2atm  34985  ps-2c  34986  lplni2  34995  lplnle  34998  lplnnle2at  34999  lplnri3N  35013  llncvrlpln2  35015  2atmat  35019  2llnm2N  35026  2llnm4  35028  2llnmeqat  35029  lvolnle3at  35040  4atlem0ae  35052  4atlem0be  35053  4atlem3b  35056  4atlem9  35061  4atlem10a  35062  4atlem10  35064  4atlem11a  35065  4atlem12a  35068  4at2  35072  2lplnm2N  35079  lneq2at  35236  2llnma1b  35244  2llnma1  35245  2llnma3r  35246  2llnma2  35247  2llnma2rN  35248  cdlema1N  35249  paddasslem2  35279  paddasslem15  35292  paddasslem16  35293  pmodlem1  35304  pmodlem2  35305  pmod2iN  35307  hlmod1i  35314  atmod1i1m  35316  atmod2i1  35319  atmod2i2  35320  atmod3i1  35322  atmod3i2  35323  atmod4i1  35324  atmod4i2  35325  llnexchb2lem  35326  llnexch2N  35328  dalawlem3  35331  dalawlem4  35332  dalawlem5  35333  dalawlem6  35334  dalawlem7  35335  dalawlem8  35336  dalawlem9  35337  dalawlem11  35339  dalawlem12  35340  dalawlem13  35341  dalawlem15  35343  osumcllem9N  35422  pl42lem1N  35437  4atexlems  35510  4atex2  35535  4atex2-0bOLDN  35537  trlval4  35647  cdlemc5  35654  cdlemc6  35655  cdlemd2  35658  cdlemd4  35660  cdlemd6  35662  cdleme00a  35668  cdleme0e  35676  cdleme3g  35693  cdleme3h  35694  cdleme3  35696  cdleme4  35697  cdleme4a  35698  cdleme5  35699  cdleme9  35712  cdleme16aN  35718  cdleme11c  35720  cdleme11e  35722  cdleme11g  35724  cdleme11h  35725  cdleme11j  35726  cdleme11k  35727  cdleme11l  35728  cdleme11  35729  cdleme12  35730  cdleme14  35732  cdleme15c  35735  cdleme16b  35738  cdleme16c  35739  cdleme16d  35740  cdleme16e  35741  cdleme16f  35742  cdleme0nex  35749  cdleme18a  35750  cdleme18c  35752  cdleme18d  35754  cdlemednpq  35758  cdlemednuN  35759  cdleme20zN  35760  cdleme20y  35761  cdleme20yOLD  35762  cdleme19a  35763  cdleme19b  35764  cdleme19d  35766  cdleme19e  35767  cdleme20aN  35769  cdleme20bN  35770  cdleme20c  35771  cdleme20d  35772  cdleme20f  35774  cdleme20g  35775  cdleme20i  35777  cdleme20j  35778  cdleme20l1  35780  cdleme20l2  35781  cdleme20l  35782  cdleme20m  35783  cdleme21b  35786  cdleme21c  35787  cdleme21e  35791  cdleme21f  35792  cdleme22a  35800  cdleme22b  35801  cdleme22e  35804  cdleme22eALTN  35805  cdleme22f  35806  cdleme26eALTN  35821  cdleme26fALTN  35822  cdleme26f  35823  cdleme26f2ALTN  35824  cdleme26f2  35825  cdleme27N  35829  cdleme28a  35830  cdleme28b  35831  cdleme30a  35838  cdleme43fsv1snlem  35880  cdlemefs31fv1  35884  cdlemefs45eN  35891  cdleme32b  35902  cdleme32c  35903  cdleme32d  35904  cdleme35h  35916  cdleme36a  35920  cdleme36m  35921  cdleme37m  35922  cdleme40m  35927  cdleme40n  35928  cdleme41sn3aw  35934  cdleme41sn4aw  35935  cdleme41fva11  35937  cdleme42k  35944  cdleme43cN  35951  cdleme43dN  35952  cdleme46f2g1  35954  cdlemeg47rv2  35970  cdlemeg46sfg  35980  cdlemeg46fjgN  35981  cdlemeg46rjgN  35982  cdlemeg46fjv  35983  cdlemeg46frv  35985  cdlemeg46vrg  35987  cdlemeg46rgv  35988  cdlemeg46req  35989  cdlemeg46gfv  35990  cdlemg4a  36068  cdlemg4d  36073  cdlemg4e  36074  cdlemg4f  36075  cdlemg4g  36076  cdlemg4  36077  cdlemg6d  36081  cdlemg6e  36082  cdlemg8b  36088  cdlemg8c  36089  cdlemg9a  36092  cdlemg9b  36093  cdlemg10a  36100  cdlemg10  36101  cdlemg12a  36103  cdlemg12b  36104  cdlemg12f  36108  cdlemg12g  36109  cdlemg12  36110  cdlemg17dN  36123  cdlemg17dALTN  36124  cdlemg17e  36125  cdlemg17f  36126  cdlemg17g  36127  cdlemg17h  36128  cdlemg17i  36129  cdlemg17pq  36132  cdlemg17iqN  36134  cdlemg17  36137  cdlemg18b  36139  cdlemg18c  36140  cdlemg19a  36143  cdlemg19  36144  cdlemg28a  36153  cdlemg27b  36156  cdlemg28b  36163  cdlemg28  36164  cdlemg33a  36166  cdlemg33b  36167  cdlemg33c  36168  cdlemg33d  36169  cdlemg33e  36170  cdlemg33  36171  cdlemg35  36173  cdlemg36  36174  cdlemg44a  36191  cdlemh  36277  cdlemi2  36279  cdlemj1  36281  tendocan  36284  cdlemk5a  36295  cdlemki  36301  cdlemkvcl  36302  cdlemk10  36303  cdlemksv2  36307  cdlemkole  36313  cdlemk14  36314  cdlemk15  36315  cdlemk16a  36316  cdlemk16  36317  cdlemk17  36318  cdlemk18  36328  cdlemk19  36329  cdlemkoatnle-2N  36335  cdlemk13-2N  36336  cdlemkole-2N  36337  cdlemk14-2N  36338  cdlemk15-2N  36339  cdlemk16-2N  36340  cdlemk17-2N  36341  cdlemk18-2N  36346  cdlemk19-2N  36347  cdlemk30  36354  cdlemk18-3N  36360  cdlemk23-3  36362  cdlemk25-3  36364  cdlemk27-3  36367  cdlemk37  36374  cdlemkfid1N  36381  cdlemkid1  36382  cdlemky  36386  cdlemk11ta  36389  cdlemk47  36409  cdlemk48  36410  cdlemk49  36411  cdlemk50  36412  cdlemk51  36413  cdlemk52  36414  cdlemk53a  36415  cdlemk54  36418  cdlemk39u1  36427  cdlemk19u1  36429  cdleml1N  36436  cdleml2N  36437  cdleml3N  36438  dia2dimlem6  36530  cdlemn2  36656  cdlemn2a  36657  cdlemn5pre  36661  cdlemn10  36667  cdlemn11c  36670  cdlemn11pre  36671  dihjustlem  36677  dihjust  36678  lclkrlem2y  36992