Theorem simp21 1063

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

Syntax hints:   -> wi 4   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  simpl21  1108  simpr21  1117  simp121  1162  simp221  1171  simp321  1180  omeulem1  7301  cofsmo  8717  axdc4lem  8903  0catg  15671  funcoppc  15858  funcres  15879  catcisolem  16079  1stfcl  16160  2ndfcl  16161  prfcl  16166  evlfcl  16185  curf1cl  16191  curfcl  16195  hofcl  16222  mulgdirlem  16860  mdetunilem4  19717  mdetuni0  19723  mdetmul  19725  prdsxmetlem  21461  isosctrlem3  23828  isosctr  23829  amgmlem  23994  f1otrg  24980  colinearalg  25019  ax5seglem6  25043  ax5seg  25047  axpasch  25050  axeuclidlem  25071  axeuclid  25072  ogrpsub  28554  ogrpaddlt  28555  ogrpsublt  28559  rhmdvd  28658  bnj1128  29871  mclspps  30294  cgrtr  30830  cgrtr3  30832  ofscom  30845  segconeq  30848  ifscgr  30882  btwnxfr  30894  colinearxfr  30913  lineext  30914  brofs2  30915  brifs2  30916  fscgr  30918  linecgr  30919  btwnconn1lem1  30925  btwnconn1lem2  30926  btwnconn1lem3  30927  btwnconn1lem4  30928  btwnconn1lem5  30929  btwnconn1lem6  30930  btwnconn1lem7  30931  seglecgr12im  30948  seglecgr12  30949  segletr  30952  broutsideof3  30964  outsideofeq  30968  lineunray  30985  lineelsb2  30986  linecom  30988  lshpkrlem5  32751  omlmod1i2N  32897  cvrnbtwn3  32913  cvrcmp  32920  cvrcmp2  32921  cvlexch2  32966  cvlexchb2  32968  cvlatexchb2  32972  cvlatexch2  32974  cvlatexch3  32975  cvlsupr7  32985  atnlej1  33015  atnlej2  33016  2llnneN  33045  cvratlem  33057  atcvrneN  33066  atcvrj1  33067  atlelt  33074  2atjm  33081  3noncolr2  33085  3noncolr1N  33086  3dimlem2  33095  3dim1  33103  3dim2  33104  1cvrat  33112  ps-1  33113  ps-2  33114  2atjlej  33115  hlatexch3N  33116  ps-2b  33118  3atlem1  33119  3atlem2  33120  3atlem5  33123  3atlem6  33124  llnle  33154  2atm  33163  ps-2c  33164  lplni2  33173  lplnle  33176  lplnnle2at  33177  lplnri3N  33191  llncvrlpln2  33193  2atmat  33197  2llnm2N  33204  2llnm4  33206  2llnmeqat  33207  lvolnle3at  33218  4atlem0ae  33230  4atlem0be  33231  4atlem3b  33234  4atlem9  33239  4atlem10a  33240  4atlem10  33242  4atlem11a  33243  4atlem12a  33246  4at2  33250  2lplnm2N  33257  lneq2at  33414  2llnma1b  33422  2llnma1  33423  2llnma3r  33424  2llnma2  33425  2llnma2rN  33426  cdlema1N  33427  paddasslem2  33457  paddasslem15  33470  paddasslem16  33471  pmodlem1  33482  pmodlem2  33483  pmod2iN  33485  hlmod1i  33492  atmod1i1m  33494  atmod2i1  33497  atmod2i2  33498  atmod3i1  33500  atmod3i2  33501  atmod4i1  33502  atmod4i2  33503  llnexchb2lem  33504  llnexch2N  33506  dalawlem3  33509  dalawlem4  33510  dalawlem5  33511  dalawlem6  33512  dalawlem7  33513  dalawlem8  33514  dalawlem9  33515  dalawlem11  33517  dalawlem12  33518  dalawlem13  33519  dalawlem15  33521  osumcllem9N  33600  pl42lem1N  33615  4atexlems  33688  4atex2  33713  4atex2-0bOLDN  33715  trlval4  33825  cdlemc5  33832  cdlemc6  33833  cdlemd2  33836  cdlemd4  33838  cdlemd6  33840  cdleme00a  33846  cdleme0e  33854  cdleme3g  33871  cdleme3h  33872  cdleme3  33874  cdleme4  33875  cdleme4a  33876  cdleme5  33877  cdleme9  33890  cdleme16aN  33896  cdleme11c  33898  cdleme11e  33900  cdleme11g  33902  cdleme11h  33903  cdleme11j  33904  cdleme11k  33905  cdleme11l  33906  cdleme11  33907  cdleme12  33908  cdleme14  33910  cdleme15c  33913  cdleme16b  33916  cdleme16c  33917  cdleme16d  33918  cdleme16e  33919  cdleme16f  33920  cdleme0nex  33927  cdleme18a  33928  cdleme18c  33930  cdleme18d  33932  cdlemednpq  33936  cdlemednuN  33937  cdleme20zN  33938  cdleme20y  33939  cdleme20yOLD  33940  cdleme19a  33941  cdleme19b  33942  cdleme19d  33944  cdleme19e  33945  cdleme20aN  33947  cdleme20bN  33948  cdleme20c  33949  cdleme20d  33950  cdleme20f  33952  cdleme20g  33953  cdleme20i  33955  cdleme20j  33956  cdleme20l1  33958  cdleme20l2  33959  cdleme20l  33960  cdleme20m  33961  cdleme21b  33964  cdleme21c  33965  cdleme21e  33969  cdleme21f  33970  cdleme22a  33978  cdleme22b  33979  cdleme22e  33982  cdleme22eALTN  33983  cdleme22f  33984  cdleme26eALTN  33999  cdleme26fALTN  34000  cdleme26f  34001  cdleme26f2ALTN  34002  cdleme26f2  34003  cdleme27N  34007  cdleme28a  34008  cdleme28b  34009  cdleme30a  34016  cdleme43fsv1snlem  34058  cdlemefs31fv1  34062  cdlemefs45eN  34069  cdleme32b  34080  cdleme32c  34081  cdleme32d  34082  cdleme35h  34094  cdleme36a  34098  cdleme36m  34099  cdleme37m  34100  cdleme40m  34105  cdleme40n  34106  cdleme41sn3aw  34112  cdleme41sn4aw  34113  cdleme41fva11  34115  cdleme42k  34122  cdleme43cN  34129  cdleme43dN  34130  cdleme46f2g1  34132  cdlemeg47rv2  34148  cdlemeg46sfg  34158  cdlemeg46fjgN  34159  cdlemeg46rjgN  34160  cdlemeg46fjv  34161  cdlemeg46frv  34163  cdlemeg46vrg  34165  cdlemeg46rgv  34166  cdlemeg46req  34167  cdlemeg46gfv  34168  cdlemg4a  34246  cdlemg4d  34251  cdlemg4e  34252  cdlemg4f  34253  cdlemg4g  34254  cdlemg4  34255  cdlemg6d  34259  cdlemg6e  34260  cdlemg8b  34266  cdlemg8c  34267  cdlemg9a  34270  cdlemg9b  34271  cdlemg10a  34278  cdlemg10  34279  cdlemg12a  34281  cdlemg12b  34282  cdlemg12f  34286  cdlemg12g  34287  cdlemg12  34288  cdlemg17dN  34301  cdlemg17dALTN  34302  cdlemg17e  34303  cdlemg17f  34304  cdlemg17g  34305  cdlemg17h  34306  cdlemg17i  34307  cdlemg17pq  34310  cdlemg17iqN  34312  cdlemg17  34315  cdlemg18b  34317  cdlemg18c  34318  cdlemg19a  34321  cdlemg19  34322  cdlemg28a  34331  cdlemg27b  34334  cdlemg28b  34341  cdlemg28  34342  cdlemg33a  34344  cdlemg33b  34345  cdlemg33c  34346  cdlemg33d  34347  cdlemg33e  34348  cdlemg33  34349  cdlemg35  34351  cdlemg36  34352  cdlemg44a  34369  cdlemh  34455  cdlemi2  34457  cdlemj1  34459  tendocan  34462  cdlemk5a  34473  cdlemki  34479  cdlemkvcl  34480  cdlemk10  34481  cdlemksv2  34485  cdlemkole  34491  cdlemk14  34492  cdlemk15  34493  cdlemk16a  34494  cdlemk16  34495  cdlemk17  34496  cdlemk18  34506  cdlemk19  34507  cdlemkoatnle-2N  34513  cdlemk13-2N  34514  cdlemkole-2N  34515  cdlemk14-2N  34516  cdlemk15-2N  34517  cdlemk16-2N  34518  cdlemk17-2N  34519  cdlemk18-2N  34524  cdlemk19-2N  34525  cdlemk30  34532  cdlemk18-3N  34538  cdlemk23-3  34540  cdlemk25-3  34542  cdlemk27-3  34545  cdlemk37  34552  cdlemkfid1N  34559  cdlemkid1  34560  cdlemky  34564  cdlemk11ta  34567  cdlemk47  34587  cdlemk48  34588  cdlemk49  34589  cdlemk50  34590  cdlemk51  34591  cdlemk52  34592  cdlemk53a  34593  cdlemk54  34596  cdlemk39u1  34605  cdlemk19u1  34607  cdleml1N  34614  cdleml2N  34615  cdleml3N  34616  dia2dimlem6  34708  cdlemn2  34834  cdlemn2a  34835  cdlemn5pre  34839  cdlemn10  34845  cdlemn11c  34848  cdlemn11pre  34849  dihjustlem  34855  dihjust  34856  lclkrlem2y  35170  relexpmulnn  36372  uhgr2edg  39453  lincreslvec3  40783