Theorem simp21 1021

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

Syntax hints:   -> wi 4   /\ w3a 965

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 967

This theorem is referenced by:  simpl21  1066  simpr21  1075  simp121  1120  simp221  1129  simp321  1138  omeulem1  7021  cofsmo  8438  axdc4lem  8624  0catg  14625  funcoppc  14785  funcres  14806  catcisolem  14974  1stfcl  15007  2ndfcl  15008  prfcl  15013  evlfcl  15032  curf1cl  15038  curfcl  15042  hofcl  15069  mulgdirlem  15651  mdetunilem4  18421  mdetuni0  18427  mdetmul  18429  prdsxmetlem  19943  isosctrlem3  22218  isosctr  22219  amgmlem  22383  f1otrg  23117  colinearalg  23156  ax5seglem6  23180  ax5seg  23184  axpasch  23187  axeuclidlem  23208  axeuclid  23209  ogrpsub  26180  ogrpsublt  26185  rhmdvd  26289  cgrtr  28023  cgrtr3  28025  ofscom  28038  segconeq  28041  ifscgr  28075  btwnxfr  28087  colinearxfr  28106  lineext  28107  brofs2  28108  brifs2  28109  fscgr  28111  linecgr  28112  btwnconn1lem1  28118  btwnconn1lem2  28119  btwnconn1lem3  28120  btwnconn1lem4  28121  btwnconn1lem5  28122  btwnconn1lem6  28123  btwnconn1lem7  28124  seglecgr12im  28141  seglecgr12  28142  segletr  28145  broutsideof3  28157  outsideofeq  28161  lineunray  28178  lineelsb2  28179  linecom  28181  bnj1128  31981  lshpkrlem5  32759  omlmod1i2N  32905  cvrnbtwn3  32921  cvrcmp  32928  cvrcmp2  32929  cvlexch2  32974  cvlexchb2  32976  cvlatexchb2  32980  cvlatexch2  32982  cvlatexch3  32983  cvlsupr7  32993  atnlej1  33023  atnlej2  33024  2llnneN  33053  cvratlem  33065  atcvrneN  33074  atcvrj1  33075  atlelt  33082  2atjm  33089  3noncolr2  33093  3noncolr1N  33094  3dimlem2  33103  3dim1  33111  3dim2  33112  1cvrat  33120  ps-1  33121  ps-2  33122  2atjlej  33123  hlatexch3N  33124  ps-2b  33126  3atlem1  33127  3atlem2  33128  3atlem5  33131  3atlem6  33132  llnle  33162  2atm  33171  ps-2c  33172  lplni2  33181  lplnle  33184  lplnnle2at  33185  lplnri3N  33199  llncvrlpln2  33201  2atmat  33205  2llnm2N  33212  2llnm4  33214  2llnmeqat  33215  lvolnle3at  33226  4atlem0ae  33238  4atlem0be  33239  4atlem3b  33242  4atlem9  33247  4atlem10a  33248  4atlem10  33250  4atlem11a  33251  4atlem12a  33254  4at2  33258  2lplnm2N  33265  lneq2at  33422  2llnma1b  33430  2llnma1  33431  2llnma3r  33432  2llnma2  33433  2llnma2rN  33434  cdlema1N  33435  paddasslem2  33465  paddasslem15  33478  paddasslem16  33479  pmodlem1  33490  pmodlem2  33491  pmod2iN  33493  hlmod1i  33500  atmod1i1m  33502  atmod2i1  33505  atmod2i2  33506  atmod3i1  33508  atmod3i2  33509  atmod4i1  33510  atmod4i2  33511  llnexchb2lem  33512  llnexch2N  33514  dalawlem3  33517  dalawlem4  33518  dalawlem5  33519  dalawlem6  33520  dalawlem7  33521  dalawlem8  33522  dalawlem9  33523  dalawlem11  33525  dalawlem12  33526  dalawlem13  33527  dalawlem15  33529  osumcllem9N  33608  pl42lem1N  33623  4atexlems  33696  4atex2  33721  4atex2-0bOLDN  33723  trlval4  33832  cdlemc5  33839  cdlemc6  33840  cdlemd2  33843  cdlemd4  33845  cdlemd6  33847  cdleme00a  33853  cdleme0e  33861  cdleme3g  33878  cdleme3h  33879  cdleme3  33881  cdleme4  33882  cdleme4a  33883  cdleme5  33884  cdleme9  33897  cdleme16aN  33903  cdleme11c  33905  cdleme11e  33907  cdleme11g  33909  cdleme11h  33910  cdleme11j  33911  cdleme11k  33912  cdleme11l  33913  cdleme11  33914  cdleme12  33915  cdleme14  33917  cdleme15c  33920  cdleme16b  33923  cdleme16c  33924  cdleme16d  33925  cdleme16e  33926  cdleme16f  33927  cdleme0nex  33934  cdleme18a  33935  cdleme18c  33937  cdleme18d  33939  cdlemednpq  33943  cdlemednuN  33944  cdleme20zN  33945  cdleme20y  33946  cdleme19a  33947  cdleme19b  33948  cdleme19d  33950  cdleme19e  33951  cdleme20aN  33953  cdleme20bN  33954  cdleme20c  33955  cdleme20d  33956  cdleme20f  33958  cdleme20g  33959  cdleme20i  33961  cdleme20j  33962  cdleme20l1  33964  cdleme20l2  33965  cdleme20l  33966  cdleme20m  33967  cdleme21b  33970  cdleme21c  33971  cdleme21e  33975  cdleme21f  33976  cdleme22a  33984  cdleme22b  33985  cdleme22e  33988  cdleme22eALTN  33989  cdleme22f  33990  cdleme26eALTN  34005  cdleme26fALTN  34006  cdleme26f  34007  cdleme26f2ALTN  34008  cdleme26f2  34009  cdleme27N  34013  cdleme28a  34014  cdleme28b  34015  cdleme30a  34022  cdleme43fsv1snlem  34064  cdlemefs31fv1  34068  cdlemefs45eN  34075  cdleme32b  34086  cdleme32c  34087  cdleme32d  34088  cdleme35h  34100  cdleme36a  34104  cdleme36m  34105  cdleme37m  34106  cdleme40m  34111  cdleme40n  34112  cdleme41sn3aw  34118  cdleme41sn4aw  34119  cdleme41fva11  34121  cdleme42k  34128  cdleme43cN  34135  cdleme43dN  34136  cdleme46f2g1  34138  cdlemeg47rv2  34154  cdlemeg46sfg  34164  cdlemeg46fjgN  34165  cdlemeg46rjgN  34166  cdlemeg46fjv  34167  cdlemeg46frv  34169  cdlemeg46vrg  34171  cdlemeg46rgv  34172  cdlemeg46req  34173  cdlemeg46gfv  34174  cdlemg4a  34252  cdlemg4d  34257  cdlemg4e  34258  cdlemg4f  34259  cdlemg4g  34260  cdlemg4  34261  cdlemg6d  34265  cdlemg6e  34266  cdlemg8b  34272  cdlemg8c  34273  cdlemg9a  34276  cdlemg9b  34277  cdlemg10a  34284  cdlemg10  34285  cdlemg12a  34287  cdlemg12b  34288  cdlemg12f  34292  cdlemg12g  34293  cdlemg12  34294  cdlemg17dN  34307  cdlemg17dALTN  34308  cdlemg17e  34309  cdlemg17f  34310  cdlemg17g  34311  cdlemg17h  34312  cdlemg17i  34313  cdlemg17pq  34316  cdlemg17iqN  34318  cdlemg17  34321  cdlemg18b  34323  cdlemg18c  34324  cdlemg19a  34327  cdlemg19  34328  cdlemg28a  34337  cdlemg27b  34340  cdlemg28b  34347  cdlemg28  34348  cdlemg33a  34350  cdlemg33b  34351  cdlemg33c  34352  cdlemg33d  34353  cdlemg33e  34354  cdlemg33  34355  cdlemg35  34357  cdlemg36  34358  cdlemg44a  34375  cdlemh  34461  cdlemi2  34463  cdlemj1  34465  tendocan  34468  cdlemk5a  34479  cdlemki  34485  cdlemkvcl  34486  cdlemk10  34487  cdlemksv2  34491  cdlemkole  34497  cdlemk14  34498  cdlemk15  34499  cdlemk16a  34500  cdlemk16  34501  cdlemk17  34502  cdlemk18  34512  cdlemk19  34513  cdlemkoatnle-2N  34519  cdlemk13-2N  34520  cdlemkole-2N  34521  cdlemk14-2N  34522  cdlemk15-2N  34523  cdlemk16-2N  34524  cdlemk17-2N  34525  cdlemk18-2N  34530  cdlemk19-2N  34531  cdlemk30  34538  cdlemk18-3N  34544  cdlemk23-3  34546  cdlemk25-3  34548  cdlemk27-3  34551  cdlemk37  34558  cdlemkfid1N  34565  cdlemkid1  34566  cdlemky  34570  cdlemk11ta  34573  cdlemk47  34593  cdlemk48  34594  cdlemk49  34595  cdlemk50  34596  cdlemk51  34597  cdlemk52  34598  cdlemk53a  34599  cdlemk54  34602  cdlemk39u1  34611  cdlemk19u1  34613  cdleml1N  34620  cdleml2N  34621  cdleml3N  34622  dia2dimlem6  34714  cdlemn2  34840  cdlemn2a  34841  cdlemn5pre  34845  cdlemn10  34851  cdlemn11c  34854  cdlemn11pre  34855  dihjustlem  34861  dihjust  34862  lclkrlem2y  35176