Theorem simp21 1039

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

Syntax hints:   -> wi 4   /\ w3a 983

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 985

This theorem is referenced by:  simpl21  1084  simpr21  1093  simp121  1138  simp221  1147  simp321  1156  omeulem1  7289  cofsmo  8701  axdc4lem  8887  0catg  15586  funcoppc  15773  funcres  15794  catcisolem  15994  1stfcl  16075  2ndfcl  16076  prfcl  16081  evlfcl  16100  curf1cl  16106  curfcl  16110  hofcl  16137  mulgdirlem  16775  mdetunilem4  19632  mdetuni0  19638  mdetmul  19640  prdsxmetlem  21375  isosctrlem3  23741  isosctr  23742  amgmlem  23907  f1otrg  24893  colinearalg  24932  ax5seglem6  24956  ax5seg  24960  axpasch  24963  axeuclidlem  24984  axeuclid  24985  ogrpsub  28481  ogrpaddlt  28482  ogrpsublt  28486  rhmdvd  28586  bnj1128  29801  mclspps  30224  cgrtr  30758  cgrtr3  30760  ofscom  30773  segconeq  30776  ifscgr  30810  btwnxfr  30822  colinearxfr  30841  lineext  30842  brofs2  30843  brifs2  30844  fscgr  30846  linecgr  30847  btwnconn1lem1  30853  btwnconn1lem2  30854  btwnconn1lem3  30855  btwnconn1lem4  30856  btwnconn1lem5  30857  btwnconn1lem6  30858  btwnconn1lem7  30859  seglecgr12im  30876  seglecgr12  30877  segletr  30880  broutsideof3  30892  outsideofeq  30896  lineunray  30913  lineelsb2  30914  linecom  30916  lshpkrlem5  32643  omlmod1i2N  32789  cvrnbtwn3  32805  cvrcmp  32812  cvrcmp2  32813  cvlexch2  32858  cvlexchb2  32860  cvlatexchb2  32864  cvlatexch2  32866  cvlatexch3  32867  cvlsupr7  32877  atnlej1  32907  atnlej2  32908  2llnneN  32937  cvratlem  32949  atcvrneN  32958  atcvrj1  32959  atlelt  32966  2atjm  32973  3noncolr2  32977  3noncolr1N  32978  3dimlem2  32987  3dim1  32995  3dim2  32996  1cvrat  33004  ps-1  33005  ps-2  33006  2atjlej  33007  hlatexch3N  33008  ps-2b  33010  3atlem1  33011  3atlem2  33012  3atlem5  33015  3atlem6  33016  llnle  33046  2atm  33055  ps-2c  33056  lplni2  33065  lplnle  33068  lplnnle2at  33069  lplnri3N  33083  llncvrlpln2  33085  2atmat  33089  2llnm2N  33096  2llnm4  33098  2llnmeqat  33099  lvolnle3at  33110  4atlem0ae  33122  4atlem0be  33123  4atlem3b  33126  4atlem9  33131  4atlem10a  33132  4atlem10  33134  4atlem11a  33135  4atlem12a  33138  4at2  33142  2lplnm2N  33149  lneq2at  33306  2llnma1b  33314  2llnma1  33315  2llnma3r  33316  2llnma2  33317  2llnma2rN  33318  cdlema1N  33319  paddasslem2  33349  paddasslem15  33362  paddasslem16  33363  pmodlem1  33374  pmodlem2  33375  pmod2iN  33377  hlmod1i  33384  atmod1i1m  33386  atmod2i1  33389  atmod2i2  33390  atmod3i1  33392  atmod3i2  33393  atmod4i1  33394  atmod4i2  33395  llnexchb2lem  33396  llnexch2N  33398  dalawlem3  33401  dalawlem4  33402  dalawlem5  33403  dalawlem6  33404  dalawlem7  33405  dalawlem8  33406  dalawlem9  33407  dalawlem11  33409  dalawlem12  33410  dalawlem13  33411  dalawlem15  33413  osumcllem9N  33492  pl42lem1N  33507  4atexlems  33580  4atex2  33605  4atex2-0bOLDN  33607  trlval4  33717  cdlemc5  33724  cdlemc6  33725  cdlemd2  33728  cdlemd4  33730  cdlemd6  33732  cdleme00a  33738  cdleme0e  33746  cdleme3g  33763  cdleme3h  33764  cdleme3  33766  cdleme4  33767  cdleme4a  33768  cdleme5  33769  cdleme9  33782  cdleme16aN  33788  cdleme11c  33790  cdleme11e  33792  cdleme11g  33794  cdleme11h  33795  cdleme11j  33796  cdleme11k  33797  cdleme11l  33798  cdleme11  33799  cdleme12  33800  cdleme14  33802  cdleme15c  33805  cdleme16b  33808  cdleme16c  33809  cdleme16d  33810  cdleme16e  33811  cdleme16f  33812  cdleme0nex  33819  cdleme18a  33820  cdleme18c  33822  cdleme18d  33824  cdlemednpq  33828  cdlemednuN  33829  cdleme20zN  33830  cdleme20y  33831  cdleme20yOLD  33832  cdleme19a  33833  cdleme19b  33834  cdleme19d  33836  cdleme19e  33837  cdleme20aN  33839  cdleme20bN  33840  cdleme20c  33841  cdleme20d  33842  cdleme20f  33844  cdleme20g  33845  cdleme20i  33847  cdleme20j  33848  cdleme20l1  33850  cdleme20l2  33851  cdleme20l  33852  cdleme20m  33853  cdleme21b  33856  cdleme21c  33857  cdleme21e  33861  cdleme21f  33862  cdleme22a  33870  cdleme22b  33871  cdleme22e  33874  cdleme22eALTN  33875  cdleme22f  33876  cdleme26eALTN  33891  cdleme26fALTN  33892  cdleme26f  33893  cdleme26f2ALTN  33894  cdleme26f2  33895  cdleme27N  33899  cdleme28a  33900  cdleme28b  33901  cdleme30a  33908  cdleme43fsv1snlem  33950  cdlemefs31fv1  33954  cdlemefs45eN  33961  cdleme32b  33972  cdleme32c  33973  cdleme32d  33974  cdleme35h  33986  cdleme36a  33990  cdleme36m  33991  cdleme37m  33992  cdleme40m  33997  cdleme40n  33998  cdleme41sn3aw  34004  cdleme41sn4aw  34005  cdleme41fva11  34007  cdleme42k  34014  cdleme43cN  34021  cdleme43dN  34022  cdleme46f2g1  34024  cdlemeg47rv2  34040  cdlemeg46sfg  34050  cdlemeg46fjgN  34051  cdlemeg46rjgN  34052  cdlemeg46fjv  34053  cdlemeg46frv  34055  cdlemeg46vrg  34057  cdlemeg46rgv  34058  cdlemeg46req  34059  cdlemeg46gfv  34060  cdlemg4a  34138  cdlemg4d  34143  cdlemg4e  34144  cdlemg4f  34145  cdlemg4g  34146  cdlemg4  34147  cdlemg6d  34151  cdlemg6e  34152  cdlemg8b  34158  cdlemg8c  34159  cdlemg9a  34162  cdlemg9b  34163  cdlemg10a  34170  cdlemg10  34171  cdlemg12a  34173  cdlemg12b  34174  cdlemg12f  34178  cdlemg12g  34179  cdlemg12  34180  cdlemg17dN  34193  cdlemg17dALTN  34194  cdlemg17e  34195  cdlemg17f  34196  cdlemg17g  34197  cdlemg17h  34198  cdlemg17i  34199  cdlemg17pq  34202  cdlemg17iqN  34204  cdlemg17  34207  cdlemg18b  34209  cdlemg18c  34210  cdlemg19a  34213  cdlemg19  34214  cdlemg28a  34223  cdlemg27b  34226  cdlemg28b  34233  cdlemg28  34234  cdlemg33a  34236  cdlemg33b  34237  cdlemg33c  34238  cdlemg33d  34239  cdlemg33e  34240  cdlemg33  34241  cdlemg35  34243  cdlemg36  34244  cdlemg44a  34261  cdlemh  34347  cdlemi2  34349  cdlemj1  34351  tendocan  34354  cdlemk5a  34365  cdlemki  34371  cdlemkvcl  34372  cdlemk10  34373  cdlemksv2  34377  cdlemkole  34383  cdlemk14  34384  cdlemk15  34385  cdlemk16a  34386  cdlemk16  34387  cdlemk17  34388  cdlemk18  34398  cdlemk19  34399  cdlemkoatnle-2N  34405  cdlemk13-2N  34406  cdlemkole-2N  34407  cdlemk14-2N  34408  cdlemk15-2N  34409  cdlemk16-2N  34410  cdlemk17-2N  34411  cdlemk18-2N  34416  cdlemk19-2N  34417  cdlemk30  34424  cdlemk18-3N  34430  cdlemk23-3  34432  cdlemk25-3  34434  cdlemk27-3  34437  cdlemk37  34444  cdlemkfid1N  34451  cdlemkid1  34452  cdlemky  34456  cdlemk11ta  34459  cdlemk47  34479  cdlemk48  34480  cdlemk49  34481  cdlemk50  34482  cdlemk51  34483  cdlemk52  34484  cdlemk53a  34485  cdlemk54  34488  cdlemk39u1  34497  cdlemk19u1  34499  cdleml1N  34506  cdleml2N  34507  cdleml3N  34508  dia2dimlem6  34600  cdlemn2  34726  cdlemn2a  34727  cdlemn5pre  34731  cdlemn10  34737  cdlemn11c  34740  cdlemn11pre  34741  dihjustlem  34747  dihjust  34748  lclkrlem2y  35062  relexpmulnn  36205  lincreslvec3  39619