Theorem simp22 1095

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

Assertion

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

Proof of Theorem simp22

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

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:  simpl22  1140  simpr22  1149  simp122  1194  simp222  1203  simp322  1212  elfiun  8336  cofsmo  9091  modexp  12999  funcoppc  16535  funcres  16556  catcisolem  16756  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  mulgdirlem  17572  pmtrprfv3  17874  mdetunilem4  20421  mdetuni0  20427  mdetmul  20429  prdsxmetlem  22173  isosctrlem3  24550  isosctr  24551  amgmlem  24716  f1otrg  25751  colinearalg  25790  ax5seglem6  25814  ax5seg  25818  axpasch  25821  axeuclidlem  25842  axeuclid  25843  ogrpsub  29717  ogrpaddlt  29718  ogrpsublt  29722  rhmdvd  29821  bnj966  31014  mclspps  31481  cgrtr  32099  cgrtr3  32101  ofscom  32114  cgrextend  32115  btwnxfr  32163  colinearxfr  32182  lineext  32183  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  linecom  32257  eqlkr  34386  lshpkrlem5  34401  omlmod1i2N  34547  cvrnbtwn3  34563  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  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  3atlem5  34773  3atlem6  34774  2atm  34813  ps-2c  34814  lplni2  34823  lplnri3N  34841  llncvrlpln2  34843  2atmat  34847  2llnm2N  34854  2llnm3N  34855  2llnm4  34856  2llnmeqat  34857  lvolnle3at  34868  4atlem0ae  34880  4atlem0be  34881  4atlem3b  34884  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem12a  34896  4at2  34900  2lplnm2N  34907  lneq2at  35064  2llnma1b  35072  2llnma1  35073  2llnma3r  35074  2llnma2  35075  2llnma2rN  35076  cdlema1N  35077  paddasslem2  35107  paddasslem16  35121  pmodlem1  35132  pmod2iN  35135  hlmod1i  35142  atmod2i1  35147  atmod2i2  35148  atmod3i1  35150  atmod3i2  35151  atmod4i1  35152  atmod4i2  35153  llnexchb2lem  35154  llnexch2N  35156  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem13  35169  dalawlem15  35171  osumcllem7N  35248  osumcllem9N  35250  pl42lem1N  35265  4atexlemswapqr  35349  4atex2  35363  4atex2-0bOLDN  35365  trlval4  35475  cdlemc5  35482  cdlemc6  35483  cdlemd2  35486  cdlemd4  35488  cdlemd6  35490  cdleme00a  35496  cdleme0e  35504  cdleme4  35525  cdleme4a  35526  cdleme5  35527  cdleme9  35540  cdleme16aN  35546  cdleme11c  35548  cdleme11dN  35549  cdleme11e  35550  cdleme11g  35552  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme11l  35556  cdleme11  35557  cdleme12  35558  cdleme13  35559  cdleme14  35560  cdleme15a  35561  cdleme15c  35563  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme17d1  35576  cdleme0nex  35577  cdleme18a  35578  cdleme18b  35579  cdleme18c  35580  cdleme18d  35582  cdlemednpq  35586  cdlemednuN  35587  cdleme20zN  35588  cdleme20y  35589  cdleme20yOLD  35590  cdleme19a  35591  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20aN  35597  cdleme20d  35600  cdleme20f  35602  cdleme20g  35603  cdleme20i  35605  cdleme20j  35606  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21b  35614  cdleme21c  35615  cdleme21e  35619  cdleme21j  35624  cdleme22aa  35627  cdleme22a  35628  cdleme22b  35629  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme30a  35666  cdlemefs31fv1  35712  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35h  35744  cdleme36a  35748  cdleme36m  35749  cdleme41sn3aw  35762  cdleme41sn4aw  35763  cdleme41fva11  35765  cdleme42k  35772  cdleme43cN  35779  cdleme46f2g1  35782  cdlemeg46fjgN  35809  cdlemeg46fjv  35811  cdlemeg46frv  35813  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfv  35818  cdleme50trn2a  35838  cdlemg4a  35896  cdlemg4d  35901  cdlemg4e  35902  cdlemg4f  35903  cdlemg8c  35917  cdlemg9a  35920  cdlemg9b  35921  cdlemg10a  35928  cdlemg10  35929  cdlemg12b  35932  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg17dN  35951  cdlemg17dALTN  35952  cdlemg17e  35953  cdlemg17f  35954  cdlemg17g  35955  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  cdlemg27b  35984  cdlemg33b0  35989  cdlemg28b  35991  cdlemg28  35992  cdlemg35  36001  cdlemg36  36002  cdlemg44a  36019  cdlemh  36105  cdlemi2  36107  cdlemj1  36109  tendocan  36112  cdlemk5a  36123  cdlemk5  36124  cdlemki  36129  cdlemkvcl  36130  cdlemk10  36131  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkoatnle  36139  cdlemk15  36143  cdlemk16a  36144  cdlemk16  36145  cdlemk1u  36147  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  cdlemkuel-3  36186  cdlemkuv2-3N  36187  cdlemk18-3N  36188  cdlemkfid1N  36209  cdlemkid1  36210  cdlemkfid3N  36213  cdlemky  36214  cdlemk11ta  36217  cdlemk47  36237  cdlemk48  36238  cdlemk49  36239  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  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  cdlemn11a  36496  dihjustlem  36505  dihjust  36506  dihmeetlem15N  36610  lclkrlem2y  36820  relexpmulnn  38001  amgmwlem  42548