Theorem simp23 1096

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp23	|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> th )

Proof of Theorem simp23

Step	Hyp	Ref	Expression
1		simp3 1063	. 2 |- ( ( ps /\ ch /\ th ) -> th )
2	1	3ad2ant2 1083	1 |- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl23  1141  simpr23  1150  simp123  1195  simp223  1204  simp323  1213  funtpgOLD  5943  omeulem1  7662  elfiun  8336  cofsmo  9091  modexp  12999  iscatd2  16342  funcoppc  16535  funcres  16556  catcisolem  16756  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  pmtrprfv3  17874  mdetunilem3  20420  mdetunilem4  20421  mdetuni0  20427  mdetmul  20429  prdsxmetlem  22173  isosctrlem3  24550  isosctr  24551  f1otrg  25751  colinearalg  25790  ax5seglem6  25814  ax5seg  25818  axpasch  25821  axeuclid  25843  uhgr2edg  26100  ogrpsub  29717  ogrpsublt  29722  rhmdvd  29821  bnj966  31014  bnj967  31015  mclspps  31481  cgrtr  32099  cgrtr3  32101  ofscom  32114  btwnxfr  32163  colinearxfr  32182  lineext  32183  brofs2  32184  brifs2  32185  fscgr  32187  linecgr  32188  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem7  32200  seglecgr12im  32217  seglecgr12  32218  segletr  32221  broutsideof3  32233  outsideofeq  32237  lineunray  32254  eqlkr  34386  omlmod1i2N  34547  cvrcmp2  34571  cvlexch2  34616  cvlexchb2  34618  cvlatexchb2  34622  cvlatexch1  34623  cvlatexch2  34624  cvlatexch3  34625  cvlsupr7  34635  cvlsupr8  34636  atnlej1  34665  atnlej2  34666  2llnneN  34695  cvratlem  34707  atcvrneN  34716  atcvrj1  34717  atlelt  34724  2atjm  34731  3noncolr2  34735  3noncolr1N  34736  hlatcon2  34738  3dimlem2  34745  3dim1  34753  3dim2  34754  1cvrat  34762  ps-1  34763  ps-2  34764  2atjlej  34765  hlatexch3N  34766  ps-2b  34768  3atlem1  34769  3atlem2  34770  3atlem6  34774  llnle  34804  2atm  34813  ps-2c  34814  lplni2  34823  lplnle  34826  lplnnle2at  34827  lplnri3N  34841  llncvrlpln2  34843  2atmat  34847  2llnjaN  34852  2llnm2N  34854  2llnm4  34856  2llnmeqat  34857  lvolnle3at  34868  4atlem0ae  34880  4atlem0be  34881  4atlem3b  34884  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem12a  34896  4at  34899  4at2  34900  lplncvrlvol2  34901  2lplnm2N  34907  2llnma1b  35072  2llnma1  35073  2llnma3r  35074  2llnma2  35075  2llnma2rN  35076  cdlema1N  35077  cdlema2N  35078  paddasslem2  35107  paddasslem15  35120  paddasslem16  35121  pmodlem1  35132  pmod2iN  35135  hlmod1i  35142  atmod2i1  35147  atmod2i2  35148  atmod3i1  35150  atmod3i2  35151  atmod4i1  35152  atmod4i2  35153  llnexchb2  35155  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem13  35169  dalawlem15  35171  osumcllem7N  35248  osumcllem9N  35250  osumcllem11N  35252  pl42lem1N  35265  4atex  35362  4atex2-0aOLDN  35364  4atex2-0bOLDN  35365  4atex2-0cOLDN  35366  trlval4  35475  cdlemc5  35482  cdlemd5  35489  cdlemd6  35490  cdleme00a  35496  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4  35525  cdleme4a  35526  cdleme16aN  35546  cdleme11c  35548  cdleme11g  35552  cdleme11h  35553  cdleme12  35558  cdleme0nex  35577  cdleme18a  35578  cdleme18b  35579  cdleme18c  35580  cdleme18d  35582  cdleme20zN  35588  cdleme20y  35589  cdleme20yOLD  35590  cdleme19a  35591  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20aN  35597  cdleme20c  35599  cdleme20d  35600  cdleme20i  35605  cdleme20j  35606  cdleme20l1  35608  cdleme20l2  35609  cdleme20m  35611  cdleme21b  35614  cdleme21c  35615  cdleme21j  35624  cdleme22aa  35627  cdleme22a  35628  cdleme22eALTN  35633  cdleme26e  35647  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme30a  35666  cdlemefs45eN  35719  cdleme32c  35731  cdleme32e  35733  cdleme35h  35744  cdleme36a  35748  cdleme36m  35749  cdleme37m  35750  cdleme41sn3aw  35762  cdleme41sn4aw  35763  cdleme41fva11  35765  cdleme42k  35772  cdleme43cN  35779  cdleme43dN  35780  cdleme46f2g1  35782  cdlemeg47rv2  35798  cdlemeg46sfg  35808  cdlemeg46fjgN  35809  cdlemeg46rjgN  35810  cdlemeg46fjv  35811  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfv  35818  cdleme50trn2a  35838  cdlemg2fv2  35888  cdlemg4a  35896  cdlemg4e  35902  cdlemg4f  35903  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg9b  35921  cdlemg9  35922  cdlemg10a  35928  cdlemg12a  35931  cdlemg12b  35932  cdlemg12c  35933  cdlemg12  35938  cdlemg17dN  35951  cdlemg17dALTN  35952  cdlemg17e  35953  cdlemg17i  35957  cdlemg17ir  35958  cdlemg17pq  35960  cdlemg17bq  35961  cdlemg17iqN  35962  cdlemg17  35965  cdlemg18b  35967  cdlemg18c  35968  cdlemg18d  35969  cdlemg18  35970  cdlemg19  35972  cdlemg21  35974  cdlemg28a  35981  cdlemg31b0a  35983  cdlemg33b0  35989  cdlemg35  36001  cdlemg44a  36019  cdlemh  36105  cdlemi2  36107  cdlemj1  36109  cdlemk5a  36123  cdlemk5  36124  cdlemki  36129  cdlemkvcl  36130  cdlemk10  36131  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemk15  36143  cdlemk16a  36144  cdlemk16  36145  cdlemk5u  36149  cdlemk6u  36150  cdlemk18  36156  cdlemk19  36157  cdlemk7u  36158  cdlemk11u  36159  cdlemk12u  36160  cdlemk21N  36161  cdlemk20  36162  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk22  36181  cdlemk30  36182  cdlemk28-3  36196  cdlemk33N  36197  cdlemkfid1N  36209  cdlemkid1  36210  cdlemky  36214  cdlemk11ta  36217  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk47  36237  cdlemk48  36238  cdlemk49  36239  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  cdlemk53b  36244  cdlemk53  36245  cdlemk54  36246  cdlemk55a  36247  cdlemkyyN  36250  cdlemk43N  36251  cdlemk55u1  36253  cdlemk55u  36254  cdlemk39u1  36255  cdlemk19u1  36257  cdleml1N  36264  cdleml2N  36265  cdleml3N  36266  dia2dimlem6  36358  cdlemn2  36484  cdlemn2a  36485  cdlemn5pre  36489  cdlemn11pre  36499  dihjustlem  36505  dihjust  36506  dihmeetlem15N  36610  lclkrlem2y  36820  relexpxpnnidm  37995