Theorem simp13 1028

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

Assertion

Ref	Expression
simp13

Proof of Theorem simp13

Step	Hyp	Ref	Expression
1		simp3 998	. 2
2	1	3ad2ant1 1017	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  simpl13  1073  simpr13  1082  simp113  1127  simp213  1136  simp313  1145  funtpg  5643  omeu  7253  ackbij1lem16  8636  dvdsgcd  14181  coprimeprodsq  14333  pythagtriplem4  14343  pythagtriplem13  14351  pythagtriplem14  14352  pythagtriplem16  14354  pythagtrip  14358  lsmpropd  16695  matsc  18952  mdetunilem7  19120  smadiadetglem2  19174  m2cpminvid  19254  pmatcollpw1lem1  19275  mp2pm2mplem2  19308  isfil2  20357  filuni  20386  ufprim  20410  cxple2a  23080  isosctr  23155  brbtwn2  24208  colinearalg  24213  ax5seg  24241  axcontlem4  24270  measres  28193  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  congmul  30905  congsub  30908  limsupre  31647  0ellimcdiv  31655  limclner  31657  lincdifsn  33025  islshpcv  34778  eqlkr  34824  lshpsmreu  34834  lshpkrlem5  34839  atlrelat1  35046  cvlcvr1  35064  cvlcvrp  35065  cvlatcvr1  35066  cvlatcvr2  35067  4noncolr3  35177  4noncolr2  35178  4noncolr1  35179  athgt  35180  3dimlem2  35183  3dimlem3a  35184  3dimlem4a  35187  3dimlem4  35188  3dimlem4OLDN  35189  3dim1  35191  3dim2  35192  hlatexch4  35205  ps-2b  35206  3atlem6  35212  llnnleat  35237  2atm  35251  ps-2c  35252  llnmlplnN  35263  2atmat  35285  2llnjN  35291  lvoli2  35305  4atlem3b  35322  4atlem10  35330  4atlem11a  35331  4atlem11b  35332  4atlem12a  35334  4atlem12b  35335  dalemswapyz  35380  lneq2at  35502  2lnat  35508  cdlema1N  35515  cdlemb  35518  pmodlem1  35570  llnmod2i2  35587  dalawlem1  35595  dalawlem3  35597  dalawlem4  35598  dalawlem6  35600  dalawlem9  35603  dalawlem10  35604  dalawlem11  35605  dalawlem12  35606  dalawlem13  35607  dalawlem15  35609  dalaw  35610  pclfinN  35624  osumcllem5N  35684  osumcllem6N  35685  osumcllem7N  35686  osumcllem9N  35688  osumcllem11N  35690  pl42lem1N  35703  lhp2at0  35756  lhp2atne  35758  lhp2at0ne  35760  4atexlem7  35799  ldilco  35840  ltrneq  35873  cdlemd2  35924  cdleme0ex2N  35949  cdleme7aa  35967  cdleme7c  35970  cdleme7d  35971  cdleme7ga  35973  cdleme11c  35986  cdleme11l  35994  cdleme11  35995  cdleme14  35998  cdleme15a  35999  cdleme15c  36001  cdleme16b  36004  cdleme16c  36005  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme0nex  36015  cdleme19b  36030  cdleme19d  36032  cdleme19e  36033  cdleme20f  36040  cdleme20k  36045  cdleme20l1  36046  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme21a  36051  cdleme21b  36052  cdleme21c  36053  cdleme21ct  36055  cdleme21d  36056  cdleme21e  36057  cdleme21f  36058  cdleme21i  36061  cdleme22cN  36068  cdleme22eALTN  36071  cdleme25a  36079  cdleme25c  36081  cdleme25dN  36082  cdleme26e  36085  cdleme26ee  36086  cdleme26eALTN  36087  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme28a  36096  cdleme28b  36097  cdleme28  36099  cdlemefr32sn2aw  36130  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32c  36169  cdleme32e  36171  cdleme32le  36173  cdleme35a  36174  cdleme35b  36176  cdleme35d  36178  cdleme36a  36186  cdleme36m  36187  cdleme39a  36191  cdleme40m  36193  cdleme40n  36194  cdleme43bN  36216  cdleme43dN  36218  cdleme46f2g2  36219  cdleme46f2g1  36220  cdleme4gfv  36233  cdlemeg49le  36237  cdlemeg46c  36239  cdlemeg46fvaw  36242  cdlemeg46nlpq  36243  cdlemeg46gfre  36258  cdleme50trn2  36277  cdlemg2ce  36318  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  cdlemg17pq  36398  cdlemg17bq  36399  cdlemg18d  36407  cdlemg19a  36409  cdlemg19  36410  cdlemg21  36412  cdlemg27a  36418  cdlemg31b0N  36420  cdlemg27b  36422  cdlemg31c  36425  cdlemg33b0  36427  cdlemg33c0  36428  cdlemg28b  36429  cdlemg33a  36432  cdlemg33  36437  ltrnco  36445  cdlemg44  36459  cdlemg47  36462  tendococl  36498  tendoplcl  36507  cdlemh1  36541  cdlemh2  36542  cdlemh  36543  cdlemi  36546  cdlemk5  36562  cdlemk6  36563  cdlemksel  36571  cdlemksv2  36573  cdlemk7  36574  cdlemk11  36575  cdlemk12  36576  cdlemkole  36579  cdlemk14  36580  cdlemk15  36581  cdlemk16a  36582  cdlemk16  36583  cdlemk1u  36585  cdlemk5u  36587  cdlemk6u  36588  cdlemkuel  36591  cdlemkuv2  36593  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  cdlemkuel-3  36624  cdlemkuv2-3N  36625  cdlemk22-3  36627  cdlemk33N  36635  cdlemk47  36675  cdlemk48  36676  cdlemk49  36677  cdlemk50  36678  cdlemk51  36679  cdlemk52  36680  cdlemk53a  36681  cdlemk55b  36686  cdlemkyyN  36688  cdlemk55u1  36691  cdlemk39u1  36693  cdlemk56  36697  dihord1  36945  dihord2a  36946  dihord10  36950  dihord11c  36951  dihord4  36985  dihord5apre  36989  dihglblem2N  37021  dihglbcpreN  37027  dihmeetlem3N  37032  dihjatc1  37038  dihjatc2N  37039  dihjatc3  37040  mapdpglem24  37431  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  hdmap14lem11  37608  hdmap14lem12  37609  hdmapglem7  37659

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