Theorem simp21 1016

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

Syntax hints:   -> wi 4   /\ w3a 960

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 962

This theorem is referenced by:  simpl21  1061  simpr21  1070  simp121  1115  simp221  1124  simp321  1133  omeulem1  7011  cofsmo  8428  axdc4lem  8614  0catg  14610  funcoppc  14770  funcres  14791  catcisolem  14959  1stfcl  14992  2ndfcl  14993  prfcl  14998  evlfcl  15017  curf1cl  15023  curfcl  15027  hofcl  15054  mulgdirlem  15633  mdetunilem4  18265  mdetuni0  18271  mdetmul  18273  prdsxmetlem  19787  isosctrlem3  22105  isosctr  22106  amgmlem  22270  f1otrg  22942  colinearalg  22981  ax5seglem6  23005  ax5seg  23009  axpasch  23012  axeuclidlem  23033  axeuclid  23034  ogrpsub  26006  ogrpsublt  26011  rhmdvd  26144  cgrtr  27872  cgrtr3  27874  ofscom  27887  segconeq  27890  ifscgr  27924  btwnxfr  27936  colinearxfr  27955  lineext  27956  brofs2  27957  brifs2  27958  fscgr  27960  linecgr  27961  btwnconn1lem1  27967  btwnconn1lem2  27968  btwnconn1lem3  27969  btwnconn1lem4  27970  btwnconn1lem5  27971  btwnconn1lem6  27972  btwnconn1lem7  27973  seglecgr12im  27990  seglecgr12  27991  segletr  27994  broutsideof3  28006  outsideofeq  28010  lineunray  28027  lineelsb2  28028  linecom  28030  bnj1128  31723  lshpkrlem5  32372  omlmod1i2N  32518  cvrnbtwn3  32534  cvrcmp  32541  cvrcmp2  32542  cvlexch2  32587  cvlexchb2  32589  cvlatexchb2  32593  cvlatexch2  32595  cvlatexch3  32596  cvlsupr7  32606  atnlej1  32636  atnlej2  32637  2llnneN  32666  cvratlem  32678  atcvrneN  32687  atcvrj1  32688  atlelt  32695  2atjm  32702  3noncolr2  32706  3noncolr1N  32707  3dimlem2  32716  3dim1  32724  3dim2  32725  1cvrat  32733  ps-1  32734  ps-2  32735  2atjlej  32736  hlatexch3N  32737  ps-2b  32739  3atlem1  32740  3atlem2  32741  3atlem5  32744  3atlem6  32745  llnle  32775  2atm  32784  ps-2c  32785  lplni2  32794  lplnle  32797  lplnnle2at  32798  lplnri3N  32812  llncvrlpln2  32814  2atmat  32818  2llnm2N  32825  2llnm4  32827  2llnmeqat  32828  lvolnle3at  32839  4atlem0ae  32851  4atlem0be  32852  4atlem3b  32855  4atlem9  32860  4atlem10a  32861  4atlem10  32863  4atlem11a  32864  4atlem12a  32867  4at2  32871  2lplnm2N  32878  lneq2at  33035  2llnma1b  33043  2llnma1  33044  2llnma3r  33045  2llnma2  33046  2llnma2rN  33047  cdlema1N  33048  paddasslem2  33078  paddasslem15  33091  paddasslem16  33092  pmodlem1  33103  pmodlem2  33104  pmod2iN  33106  hlmod1i  33113  atmod1i1m  33115  atmod2i1  33118  atmod2i2  33119  atmod3i1  33121  atmod3i2  33122  atmod4i1  33123  atmod4i2  33124  llnexchb2lem  33125  llnexch2N  33127  dalawlem3  33130  dalawlem4  33131  dalawlem5  33132  dalawlem6  33133  dalawlem7  33134  dalawlem8  33135  dalawlem9  33136  dalawlem11  33138  dalawlem12  33139  dalawlem13  33140  dalawlem15  33142  osumcllem9N  33221  pl42lem1N  33236  4atexlems  33309  4atex2  33334  4atex2-0bOLDN  33336  trlval4  33445  cdlemc5  33452  cdlemc6  33453  cdlemd2  33456  cdlemd4  33458  cdlemd6  33460  cdleme00a  33466  cdleme0e  33474  cdleme3g  33491  cdleme3h  33492  cdleme3  33494  cdleme4  33495  cdleme4a  33496  cdleme5  33497  cdleme9  33510  cdleme16aN  33516  cdleme11c  33518  cdleme11e  33520  cdleme11g  33522  cdleme11h  33523  cdleme11j  33524  cdleme11k  33525  cdleme11l  33526  cdleme11  33527  cdleme12  33528  cdleme14  33530  cdleme15c  33533  cdleme16b  33536  cdleme16c  33537  cdleme16d  33538  cdleme16e  33539  cdleme16f  33540  cdleme0nex  33547  cdleme18a  33548  cdleme18c  33550  cdleme18d  33552  cdlemednpq  33556  cdlemednuN  33557  cdleme20zN  33558  cdleme20y  33559  cdleme19a  33560  cdleme19b  33561  cdleme19d  33563  cdleme19e  33564  cdleme20aN  33566  cdleme20bN  33567  cdleme20c  33568  cdleme20d  33569  cdleme20f  33571  cdleme20g  33572  cdleme20i  33574  cdleme20j  33575  cdleme20l1  33577  cdleme20l2  33578  cdleme20l  33579  cdleme20m  33580  cdleme21b  33583  cdleme21c  33584  cdleme21e  33588  cdleme21f  33589  cdleme22a  33597  cdleme22b  33598  cdleme22e  33601  cdleme22eALTN  33602  cdleme22f  33603  cdleme26eALTN  33618  cdleme26fALTN  33619  cdleme26f  33620  cdleme26f2ALTN  33621  cdleme26f2  33622  cdleme27N  33626  cdleme28a  33627  cdleme28b  33628  cdleme30a  33635  cdleme43fsv1snlem  33677  cdlemefs31fv1  33681  cdlemefs45eN  33688  cdleme32b  33699  cdleme32c  33700  cdleme32d  33701  cdleme35h  33713  cdleme36a  33717  cdleme36m  33718  cdleme37m  33719  cdleme40m  33724  cdleme40n  33725  cdleme41sn3aw  33731  cdleme41sn4aw  33732  cdleme41fva11  33734  cdleme42k  33741  cdleme43cN  33748  cdleme43dN  33749  cdleme46f2g1  33751  cdlemeg47rv2  33767  cdlemeg46sfg  33777  cdlemeg46fjgN  33778  cdlemeg46rjgN  33779  cdlemeg46fjv  33780  cdlemeg46frv  33782  cdlemeg46vrg  33784  cdlemeg46rgv  33785  cdlemeg46req  33786  cdlemeg46gfv  33787  cdlemg4a  33865  cdlemg4d  33870  cdlemg4e  33871  cdlemg4f  33872  cdlemg4g  33873  cdlemg4  33874  cdlemg6d  33878  cdlemg6e  33879  cdlemg8b  33885  cdlemg8c  33886  cdlemg9a  33889  cdlemg9b  33890  cdlemg10a  33897  cdlemg10  33898  cdlemg12a  33900  cdlemg12b  33901  cdlemg12f  33905  cdlemg12g  33906  cdlemg12  33907  cdlemg17dN  33920  cdlemg17dALTN  33921  cdlemg17e  33922  cdlemg17f  33923  cdlemg17g  33924  cdlemg17h  33925  cdlemg17i  33926  cdlemg17pq  33929  cdlemg17iqN  33931  cdlemg17  33934  cdlemg18b  33936  cdlemg18c  33937  cdlemg19a  33940  cdlemg19  33941  cdlemg28a  33950  cdlemg27b  33953  cdlemg28b  33960  cdlemg28  33961  cdlemg33a  33963  cdlemg33b  33964  cdlemg33c  33965  cdlemg33d  33966  cdlemg33e  33967  cdlemg33  33968  cdlemg35  33970  cdlemg36  33971  cdlemg44a  33988  cdlemh  34074  cdlemi2  34076  cdlemj1  34078  tendocan  34081  cdlemk5a  34092  cdlemki  34098  cdlemkvcl  34099  cdlemk10  34100  cdlemksv2  34104  cdlemkole  34110  cdlemk14  34111  cdlemk15  34112  cdlemk16a  34113  cdlemk16  34114  cdlemk17  34115  cdlemk18  34125  cdlemk19  34126  cdlemkoatnle-2N  34132  cdlemk13-2N  34133  cdlemkole-2N  34134  cdlemk14-2N  34135  cdlemk15-2N  34136  cdlemk16-2N  34137  cdlemk17-2N  34138  cdlemk18-2N  34143  cdlemk19-2N  34144  cdlemk30  34151  cdlemk18-3N  34157  cdlemk23-3  34159  cdlemk25-3  34161  cdlemk27-3  34164  cdlemk37  34171  cdlemkfid1N  34178  cdlemkid1  34179  cdlemky  34183  cdlemk11ta  34186  cdlemk47  34206  cdlemk48  34207  cdlemk49  34208  cdlemk50  34209  cdlemk51  34210  cdlemk52  34211  cdlemk53a  34212  cdlemk54  34215  cdlemk39u1  34224  cdlemk19u1  34226  cdleml1N  34233  cdleml2N  34234  cdleml3N  34235  dia2dimlem6  34327  cdlemn2  34453  cdlemn2a  34454  cdlemn5pre  34458  cdlemn10  34464  cdlemn11c  34467  cdlemn11pre  34468  dihjustlem  34474  dihjust  34475  lclkrlem2y  34789