Theorem simp12 1027

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

Assertion

Ref	Expression
simp12

Proof of Theorem simp12

Step	Hyp	Ref	Expression
1		simp2 997	. 2
2	1	3ad2ant1 1017	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  simpl12  1072  simpr12  1081  simp112  1126  simp212  1135  simp312  1144  dvdsgcd  14181  coprimeprodsq  14333  pythagtriplem4  14343  pythagtriplem13  14351  pythagtriplem14  14352  pythagtriplem16  14354  pythagtrip  14358  pceu  14370  mremre  15001  lsmpropd  16695  m2cpminvid  19254  decpmatid  19271  mply1topmatcllem  19304  cmpsublem  19899  isfil2  20357  cxple2a  23080  isosctr  23155  brbtwn2  24208  colinearalg  24213  ax5seg  24241  axcontlem4  24270  bayesth  28378  ofscom  29657  btwndiff  29677  ifscgr  29694  brofs2  29727  brifs2  29728  fscgr  29730  btwnconn1lem1  29737  btwnconn1lem2  29738  btwnconn1lem3  29739  btwnconn1lem4  29740  btwnconn1lem12  29748  seglecgr12im  29760  seglecgr12  29761  ivthALT  30153  mzpsubst  30681  monotuz  30877  congmul  30905  congsub  30908  mullimc  31622  mullimcf  31629  0ellimcdiv  31655  limclner  31657  lincdifsn  33025  bnj1204  34068  bnj1279  34074  islshpcv  34778  lkrshp  34830  lshpsmreu  34834  lshpkrlem5  34839  cvrval3  35137  4noncolr3  35177  4noncolr2  35178  4noncolr1  35179  athgt  35180  3dimlem2  35183  3dimlem3a  35184  3dimlem4a  35187  3dimlem4  35188  3dimlem4OLDN  35189  1cvratex  35197  hlatexch4  35205  ps-2b  35206  3atlem4  35210  llnnleat  35237  2atm  35251  ps-2c  35252  llnmlplnN  35263  lplnnlelln  35267  2atmat  35285  lvoli2  35305  lvolnlelln  35308  4atlem3b  35322  4atlem10  35330  4atlem11a  35331  4atlem11b  35332  4atlem12a  35334  lplncvrlvol2  35339  2lplnja  35343  dalemswapyz  35380  lneq2at  35502  2lnat  35508  cdlema1N  35515  cdlemb  35518  paddasslem15  35558  pmodlem1  35570  llnmod2i2  35587  llnexchb2lem  35592  dalawlem1  35595  dalawlem3  35597  dalawlem4  35598  dalawlem6  35600  dalawlem7  35601  dalawlem9  35603  dalawlem10  35604  dalawlem11  35605  dalawlem12  35606  dalawlem13  35607  dalawlem15  35609  osumcllem5N  35684  osumcllem6N  35685  osumcllem7N  35686  osumcllem9N  35688  osumcllem10N  35689  osumcllem11N  35690  pl42lem1N  35703  lhpmcvr5N  35751  lhp2atne  35758  lhp2at0ne  35760  4atexlempw  35773  4atexlemex6  35798  4atexlem7  35799  ldilco  35840  ltrneq  35873  trlval2  35888  trlnidat  35898  cdlemd7  35929  cdleme7aa  35967  cdleme7c  35970  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme7  35974  cdleme11c  35986  cdleme11e  35988  cdleme11l  35994  cdleme11  35995  cdleme14  35998  cdleme15a  35999  cdleme15c  36001  cdleme16b  36004  cdleme16c  36005  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme0nex  36015  cdleme18d  36020  cdleme19b  36030  cdleme19d  36032  cdleme19e  36033  cdleme20f  36040  cdleme20k  36045  cdleme20l1  36046  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme21a  36051  cdleme21b  36052  cdleme21ct  36055  cdleme21d  36056  cdleme21e  36057  cdleme21f  36058  cdleme21h  36060  cdleme21i  36061  cdleme22eALTN  36071  cdleme22f2  36073  cdleme22g  36074  cdleme24  36078  cdleme25a  36079  cdleme25c  36081  cdleme25dN  36082  cdleme26e  36085  cdleme26ee  36086  cdleme26eALTN  36087  cdleme27N  36095  cdleme28a  36096  cdleme28b  36097  cdleme28  36099  cdlemefr32sn2aw  36130  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32c  36169  cdleme32e  36171  cdleme32le  36173  cdleme35a  36174  cdleme35b  36176  cdleme35c  36177  cdleme35e  36179  cdleme35f  36180  cdleme36a  36186  cdleme36m  36187  cdleme39a  36191  cdleme40m  36193  cdleme40n  36194  cdleme43bN  36216  cdleme43dN  36218  cdleme46f2g2  36219  cdleme46f2g1  36220  cdleme17d2  36221  cdleme4gfv  36233  cdlemeg49le  36237  cdlemeg46c  36239  cdlemeg46fvaw  36242  cdlemeg46nlpq  36243  cdlemeg46gfre  36258  cdleme50trn2  36277  cdleme  36286  cdlemg2idN  36322  cdlemg7fvbwN  36333  cdlemg10bALTN  36362  cdlemg10a  36366  cdlemg12d  36372  cdlemg12g  36375  cdlemg12  36376  cdlemg13a  36377  cdlemg13  36378  cdlemg17b  36388  cdlemg17dN  36389  cdlemg17dALTN  36390  cdlemg17e  36391  cdlemg17f  36392  cdlemg17i  36395  cdlemg17pq  36398  cdlemg17bq  36399  cdlemg17iqN  36400  cdlemg18d  36407  cdlemg18  36408  cdlemg19a  36409  cdlemg19  36410  cdlemg21  36412  cdlemg27a  36418  cdlemg28a  36419  cdlemg31b0N  36420  cdlemg27b  36422  cdlemg31c  36425  cdlemg33b0  36427  cdlemg33c0  36428  cdlemg28  36430  cdlemg33a  36432  cdlemg33  36437  cdlemg36  36440  ltrnco  36445  cdlemg44  36459  cdlemg47  36462  tendococl  36498  tendoplcl  36507  cdlemh1  36541  cdlemh2  36542  cdlemh  36543  cdlemi  36546  tendocan  36550  cdlemk5  36562  cdlemk6  36563  cdlemk7  36574  cdlemk11  36575  cdlemk12  36576  cdlemkole  36579  cdlemk14  36580  cdlemk15  36581  cdlemk16a  36582  cdlemk16  36583  cdlemk18  36594  cdlemk19  36595  cdlemk7u  36596  cdlemk11u  36597  cdlemk12u  36598  cdlemk21N  36599  cdlemk20  36600  cdlemkoatnle-2N  36601  cdlemk13-2N  36602  cdlemkole-2N  36603  cdlemk14-2N  36604  cdlemk15-2N  36605  cdlemk16-2N  36606  cdlemk17-2N  36607  cdlemk18-2N  36612  cdlemk19-2N  36613  cdlemk7u-2N  36614  cdlemk11u-2N  36615  cdlemk12u-2N  36616  cdlemk21-2N  36617  cdlemk20-2N  36618  cdlemk22  36619  cdlemk27-3  36633  cdlemk33N  36635  cdlemk11ta  36655  cdlemkid3N  36659  cdlemk11tc  36671  cdlemk11t  36672  cdlemk45  36673  cdlemk46  36674  cdlemk47  36675  cdlemk48  36676  cdlemk49  36677  cdlemk50  36678  cdlemk51  36679  cdlemk52  36680  cdlemk53a  36681  cdlemk55b  36686  cdlemkyyN  36688  cdlemk55u1  36691  cdlemk39u1  36693  cdlemk56  36697  cdlemm10N  36845  dihord1  36945  dihord2a  36946  dihord2b  36947  dihord10  36950  dihord4  36985  dihord5apre  36989  dihglblem2N  37021  dihjatc1  37038  dihjatc2N  37039  dihjatc3  37040  dihmeetlem15N  37048  dihmeetlem20N  37053  mapdpglem24  37431  hdmap14lem11  37608  hdmap14lem12  37609

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