Theorem simp21 1029

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  simpl21  1074  simpr21  1083  simp121  1128  simp221  1137  simp321  1146  omeulem1  7231  cofsmo  8649  axdc4lem  8835  0catg  14942  funcoppc  15102  funcres  15123  catcisolem  15291  1stfcl  15324  2ndfcl  15325  prfcl  15330  evlfcl  15349  curf1cl  15355  curfcl  15359  hofcl  15386  mulgdirlem  15976  mdetunilem4  18912  mdetuni0  18918  mdetmul  18920  prdsxmetlem  20634  isosctrlem3  22910  isosctr  22911  amgmlem  23075  f1otrg  23878  colinearalg  23917  ax5seglem6  23941  ax5seg  23945  axpasch  23948  axeuclidlem  23969  axeuclid  23970  ogrpsub  27397  ogrpsublt  27402  rhmdvd  27502  cgrtr  29247  cgrtr3  29249  ofscom  29262  segconeq  29265  ifscgr  29299  btwnxfr  29311  colinearxfr  29330  lineext  29331  brofs2  29332  brifs2  29333  fscgr  29335  linecgr  29336  btwnconn1lem1  29342  btwnconn1lem2  29343  btwnconn1lem3  29344  btwnconn1lem4  29345  btwnconn1lem5  29346  btwnconn1lem6  29347  btwnconn1lem7  29348  seglecgr12im  29365  seglecgr12  29366  segletr  29369  broutsideof3  29381  outsideofeq  29385  lineunray  29402  lineelsb2  29403  linecom  29405  bnj1128  33143  lshpkrlem5  33929  omlmod1i2N  34075  cvrnbtwn3  34091  cvrcmp  34098  cvrcmp2  34099  cvlexch2  34144  cvlexchb2  34146  cvlatexchb2  34150  cvlatexch2  34152  cvlatexch3  34153  cvlsupr7  34163  atnlej1  34193  atnlej2  34194  2llnneN  34223  cvratlem  34235  atcvrneN  34244  atcvrj1  34245  atlelt  34252  2atjm  34259  3noncolr2  34263  3noncolr1N  34264  3dimlem2  34273  3dim1  34281  3dim2  34282  1cvrat  34290  ps-1  34291  ps-2  34292  2atjlej  34293  hlatexch3N  34294  ps-2b  34296  3atlem1  34297  3atlem2  34298  3atlem5  34301  3atlem6  34302  llnle  34332  2atm  34341  ps-2c  34342  lplni2  34351  lplnle  34354  lplnnle2at  34355  lplnri3N  34369  llncvrlpln2  34371  2atmat  34375  2llnm2N  34382  2llnm4  34384  2llnmeqat  34385  lvolnle3at  34396  4atlem0ae  34408  4atlem0be  34409  4atlem3b  34412  4atlem9  34417  4atlem10a  34418  4atlem10  34420  4atlem11a  34421  4atlem12a  34424  4at2  34428  2lplnm2N  34435  lneq2at  34592  2llnma1b  34600  2llnma1  34601  2llnma3r  34602  2llnma2  34603  2llnma2rN  34604  cdlema1N  34605  paddasslem2  34635  paddasslem15  34648  paddasslem16  34649  pmodlem1  34660  pmodlem2  34661  pmod2iN  34663  hlmod1i  34670  atmod1i1m  34672  atmod2i1  34675  atmod2i2  34676  atmod3i1  34678  atmod3i2  34679  atmod4i1  34680  atmod4i2  34681  llnexchb2lem  34682  llnexch2N  34684  dalawlem3  34687  dalawlem4  34688  dalawlem5  34689  dalawlem6  34690  dalawlem7  34691  dalawlem8  34692  dalawlem9  34693  dalawlem11  34695  dalawlem12  34696  dalawlem13  34697  dalawlem15  34699  osumcllem9N  34778  pl42lem1N  34793  4atexlems  34866  4atex2  34891  4atex2-0bOLDN  34893  trlval4  35002  cdlemc5  35009  cdlemc6  35010  cdlemd2  35013  cdlemd4  35015  cdlemd6  35017  cdleme00a  35023  cdleme0e  35031  cdleme3g  35048  cdleme3h  35049  cdleme3  35051  cdleme4  35052  cdleme4a  35053  cdleme5  35054  cdleme9  35067  cdleme16aN  35073  cdleme11c  35075  cdleme11e  35077  cdleme11g  35079  cdleme11h  35080  cdleme11j  35081  cdleme11k  35082  cdleme11l  35083  cdleme11  35084  cdleme12  35085  cdleme14  35087  cdleme15c  35090  cdleme16b  35093  cdleme16c  35094  cdleme16d  35095  cdleme16e  35096  cdleme16f  35097  cdleme0nex  35104  cdleme18a  35105  cdleme18c  35107  cdleme18d  35109  cdlemednpq  35113  cdlemednuN  35114  cdleme20zN  35115  cdleme20y  35116  cdleme19a  35117  cdleme19b  35118  cdleme19d  35120  cdleme19e  35121  cdleme20aN  35123  cdleme20bN  35124  cdleme20c  35125  cdleme20d  35126  cdleme20f  35128  cdleme20g  35129  cdleme20i  35131  cdleme20j  35132  cdleme20l1  35134  cdleme20l2  35135  cdleme20l  35136  cdleme20m  35137  cdleme21b  35140  cdleme21c  35141  cdleme21e  35145  cdleme21f  35146  cdleme22a  35154  cdleme22b  35155  cdleme22e  35158  cdleme22eALTN  35159  cdleme22f  35160  cdleme26eALTN  35175  cdleme26fALTN  35176  cdleme26f  35177  cdleme26f2ALTN  35178  cdleme26f2  35179  cdleme27N  35183  cdleme28a  35184  cdleme28b  35185  cdleme30a  35192  cdleme43fsv1snlem  35234  cdlemefs31fv1  35238  cdlemefs45eN  35245  cdleme32b  35256  cdleme32c  35257  cdleme32d  35258  cdleme35h  35270  cdleme36a  35274  cdleme36m  35275  cdleme37m  35276  cdleme40m  35281  cdleme40n  35282  cdleme41sn3aw  35288  cdleme41sn4aw  35289  cdleme41fva11  35291  cdleme42k  35298  cdleme43cN  35305  cdleme43dN  35306  cdleme46f2g1  35308  cdlemeg47rv2  35324  cdlemeg46sfg  35334  cdlemeg46fjgN  35335  cdlemeg46rjgN  35336  cdlemeg46fjv  35337  cdlemeg46frv  35339  cdlemeg46vrg  35341  cdlemeg46rgv  35342  cdlemeg46req  35343  cdlemeg46gfv  35344  cdlemg4a  35422  cdlemg4d  35427  cdlemg4e  35428  cdlemg4f  35429  cdlemg4g  35430  cdlemg4  35431  cdlemg6d  35435  cdlemg6e  35436  cdlemg8b  35442  cdlemg8c  35443  cdlemg9a  35446  cdlemg9b  35447  cdlemg10a  35454  cdlemg10  35455  cdlemg12a  35457  cdlemg12b  35458  cdlemg12f  35462  cdlemg12g  35463  cdlemg12  35464  cdlemg17dN  35477  cdlemg17dALTN  35478  cdlemg17e  35479  cdlemg17f  35480  cdlemg17g  35481  cdlemg17h  35482  cdlemg17i  35483  cdlemg17pq  35486  cdlemg17iqN  35488  cdlemg17  35491  cdlemg18b  35493  cdlemg18c  35494  cdlemg19a  35497  cdlemg19  35498  cdlemg28a  35507  cdlemg27b  35510  cdlemg28b  35517  cdlemg28  35518  cdlemg33a  35520  cdlemg33b  35521  cdlemg33c  35522  cdlemg33d  35523  cdlemg33e  35524  cdlemg33  35525  cdlemg35  35527  cdlemg36  35528  cdlemg44a  35545  cdlemh  35631  cdlemi2  35633  cdlemj1  35635  tendocan  35638  cdlemk5a  35649  cdlemki  35655  cdlemkvcl  35656  cdlemk10  35657  cdlemksv2  35661  cdlemkole  35667  cdlemk14  35668  cdlemk15  35669  cdlemk16a  35670  cdlemk16  35671  cdlemk17  35672  cdlemk18  35682  cdlemk19  35683  cdlemkoatnle-2N  35689  cdlemk13-2N  35690  cdlemkole-2N  35691  cdlemk14-2N  35692  cdlemk15-2N  35693  cdlemk16-2N  35694  cdlemk17-2N  35695  cdlemk18-2N  35700  cdlemk19-2N  35701  cdlemk30  35708  cdlemk18-3N  35714  cdlemk23-3  35716  cdlemk25-3  35718  cdlemk27-3  35721  cdlemk37  35728  cdlemkfid1N  35735  cdlemkid1  35736  cdlemky  35740  cdlemk11ta  35743  cdlemk47  35763  cdlemk48  35764  cdlemk49  35765  cdlemk50  35766  cdlemk51  35767  cdlemk52  35768  cdlemk53a  35769  cdlemk54  35772  cdlemk39u1  35781  cdlemk19u1  35783  cdleml1N  35790  cdleml2N  35791  cdleml3N  35792  dia2dimlem6  35884  cdlemn2  36010  cdlemn2a  36011  cdlemn5pre  36015  cdlemn10  36021  cdlemn11c  36024  cdlemn11pre  36025  dihjustlem  36031  dihjust  36032  lclkrlem2y  36346