Theorem simp11 1202

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

Assertion

Ref	Expression
simp11	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Proof of Theorem simp11

Step	Hyp	Ref	Expression
1		simp1 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1132	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp111  1301  simp211  1310  simp311  1319  omeulem1  8484  omeu  8487  ackbij1lem16  10092  coprimeprodsq  16606  pythagtriplem14  16626  pythagtrip  16632  mrelatglb  18375  subglsm  19374  lsmpropd  19378  mdetmul  21878  decpmatid  22025  isfil2  23113  filuni  23142  cxple2a  25960  isosctr  26077  nolesgn2o  26925  nolesgn2ores  26926  nogesgn1o  26927  nogesgn1ores  26928  nolt02o  26949  nogt01o  26950  sslttr  27052  brbtwn2  27562  colinearalg  27567  ax5seglem3  27588  clwwlknonex2  28761  measres  32488  bayesth  32706  cofcut2  34187  ofscom  34405  btwndiff  34425  ifscgr  34442  brofs2  34475  brifs2  34476  fscgr  34478  btwnconn1lem1  34485  btwnconn1lem2  34486  btwnconn1lem3  34487  btwnconn1lem4  34488  btwnconn1lem5  34489  btwnconn1lem6  34490  btwnconn1lem7  34491  btwnconn1lem8  34492  btwnconn1lem9  34493  btwnconn1lem10  34494  btwnconn1lem11  34495  btwnconn1lem12  34496  seglecgr12im  34508  seglecgr12  34509  ivthALT  34620  eqlkr  37366  lkrshp  37372  lshpkrlem5  37381  cvrval3  37681  4noncolr3  37721  4noncolr2  37722  4noncolr1  37723  athgt  37724  3dimlem2  37727  3dimlem3a  37728  3dimlem4a  37731  3dimlem4  37732  3dimlem4OLDN  37733  3dim2  37736  1cvratex  37741  hlatexch4  37749  ps-2b  37750  3atlem1  37751  3atlem2  37752  3atlem4  37754  3atlem5  37755  3atlem6  37756  llnnleat  37781  2atm  37795  ps-2c  37796  llnmlplnN  37807  lplnnlelln  37811  2atmat  37829  2llnjN  37835  lvoli2  37849  lvolnlelln  37852  4atlem3b  37866  4atlem9  37871  4atlem10a  37872  4atlem10  37874  4atlem11a  37875  4atlem11b  37876  4atlem12a  37878  4atlem12b  37879  4at  37881  4at2  37882  lplncvrlvol2  37883  2lplnj  37888  dalemswapyz  37924  dath2  38005  lneq2at  38046  2lnat  38052  cdlema1N  38059  cdlemb  38062  paddasslem15  38102  pmodlem1  38114  llnmod2i2  38131  llnexchb2lem  38136  llnexchb2  38137  dalawlem1  38139  dalawlem3  38141  dalawlem4  38142  dalawlem5  38143  dalawlem6  38144  dalawlem7  38145  dalawlem8  38146  dalawlem9  38147  dalawlem10  38148  dalawlem11  38149  dalawlem12  38150  dalawlem13  38151  dalawlem15  38153  dalaw  38154  osumcllem5N  38228  osumcllem6N  38229  osumcllem7N  38230  osumcllem9N  38232  osumcllem10N  38233  osumcllem11N  38234  pl42lem1N  38247  lhpexle3lem  38279  lhpmcvr5N  38295  lhp2atne  38302  lhp2at0ne  38304  4atexlemswapqr  38331  4atexlemex6  38342  ldilco  38384  ltrneq  38417  trlval2  38431  trlnidat  38441  cdlemd2  38467  cdlemd7  38472  cdlemd8  38473  cdleme7aa  38510  cdleme7c  38513  cdleme7d  38514  cdleme7e  38515  cdleme7ga  38516  cdleme7  38517  cdleme11c  38529  cdleme11e  38531  cdleme11l  38537  cdleme11  38538  cdleme14  38541  cdleme15a  38542  cdleme15c  38544  cdleme16b  38547  cdleme16c  38548  cdleme16d  38549  cdleme16e  38550  cdleme16f  38551  cdleme0nex  38558  cdleme18d  38563  cdleme19b  38572  cdleme19d  38574  cdleme19e  38575  cdleme20f  38582  cdleme20i  38585  cdleme20k  38587  cdleme20l1  38588  cdleme20l2  38589  cdleme20l  38590  cdleme20m  38591  cdleme21a  38593  cdleme21b  38594  cdleme21ct  38597  cdleme21d  38598  cdleme21e  38599  cdleme21f  38600  cdleme21h  38602  cdleme22eALTN  38613  cdleme22f2  38615  cdleme22g  38616  cdleme26e  38627  cdleme26eALTN  38629  cdleme26fALTN  38630  cdleme26f  38631  cdleme26f2ALTN  38632  cdleme26f2  38633  cdleme28a  38638  cdleme28b  38639  cdleme28  38641  cdleme29ex  38642  cdleme29c  38644  cdlemefrs29cpre1  38666  cdlemefr29exN  38670  cdlemefr32sn2aw  38672  cdlemefr29bpre0N  38674  cdlemefr29clN  38675  cdlemefr32fvaN  38677  cdlemefr32fva1  38678  cdlemefs32sn1aw  38682  cdleme43fsv1snlem  38688  cdleme41sn3a  38701  cdleme32fva  38705  cdleme32b  38710  cdleme32d  38712  cdleme32e  38713  cdleme32f  38714  cdleme32le  38715  cdleme35a  38716  cdleme35fnpq  38717  cdleme35b  38718  cdleme35c  38719  cdleme35d  38720  cdleme35e  38721  cdleme35f  38722  cdleme36a  38728  cdleme36m  38729  cdleme37m  38730  cdleme39a  38733  cdleme39n  38734  cdleme40m  38735  cdleme40n  38736  cdleme42e  38747  cdleme42f  38748  cdleme42g  38749  cdleme43bN  38758  cdleme43cN  38759  cdleme43dN  38760  cdleme46f2g2  38761  cdleme46f2g1  38762  cdleme17d2  38763  cdleme48b  38771  cdleme4gfv  38775  cdlemeg49le  38779  cdlemeg46c  38781  cdlemeg46fvaw  38784  cdlemeg46nlpq  38785  cdlemeg46frv  38793  cdlemeg46rgv  38796  cdlemeg46req  38797  cdlemeg46gfre  38800  cdleme50trn1  38817  cdleme50trn2a  38818  cdleme50trn2  38819  cdleme  38828  cdlemf  38831  trlord  38837  cdlemg2ce  38860  cdlemg7fvbwN  38875  cdlemg7aN  38893  cdlemg10bALTN  38904  cdlemg10a  38908  cdlemg10  38909  cdlemg12d  38914  cdlemg12f  38916  cdlemg12g  38917  cdlemg12  38918  cdlemg13a  38919  cdlemg13  38920  cdlemg17b  38930  cdlemg17dN  38931  cdlemg17dALTN  38932  cdlemg17e  38933  cdlemg17f  38934  cdlemg17g  38935  cdlemg17h  38936  cdlemg17i  38937  cdlemg17pq  38940  cdlemg17bq  38941  cdlemg17iqN  38942  cdlemg17  38945  cdlemg18d  38949  cdlemg18  38950  cdlemg19a  38951  cdlemg19  38952  cdlemg21  38954  cdlemg27a  38960  cdlemg28a  38961  cdlemg31b0N  38962  cdlemg27b  38964  cdlemg33b0  38969  cdlemg28b  38971  cdlemg28  38972  cdlemg33a  38974  cdlemg33  38979  cdlemg34  38980  cdlemg35  38981  cdlemg36  38982  ltrnco  38987  trlcone  38996  cdlemg44  39001  cdlemg47  39004  cdlemg48  39005  tendococl  39040  tendoplcl  39049  cdlemh1  39083  cdlemi  39088  cdlemj1  39089  cdlemj2  39090  tendocan  39092  cdlemk6  39105  cdlemki  39109  cdlemksat  39114  cdlemksv2  39115  cdlemk7  39116  cdlemk11  39117  cdlemk12  39118  cdlemkoatnle  39119  cdlemkole  39121  cdlemk14  39122  cdlemk15  39123  cdlemk16a  39124  cdlemk16  39125  cdlemk17  39126  cdlemk1u  39127  cdlemk5u  39129  cdlemk6u  39130  cdlemkuat  39134  cdlemk18  39136  cdlemk19  39137  cdlemk12u  39140  cdlemk21N  39141  cdlemk20  39142  cdlemkoatnle-2N  39143  cdlemk13-2N  39144  cdlemkole-2N  39145  cdlemk14-2N  39146  cdlemk15-2N  39147  cdlemk16-2N  39148  cdlemk17-2N  39149  cdlemk18-2N  39154  cdlemk19-2N  39155  cdlemk7u-2N  39156  cdlemk11u-2N  39157  cdlemk12u-2N  39158  cdlemk21-2N  39159  cdlemk20-2N  39160  cdlemk22  39161  cdlemk23-3  39170  cdlemk25-3  39172  cdlemk26b-3  39173  cdlemk27-3  39175  cdlemk28-3  39176  cdlemk33N  39177  cdlemk37  39182  cdlemky  39194  cdlemk11ta  39197  cdlemkid3N  39201  cdlemk11tc  39213  cdlemk11t  39214  cdlemk45  39215  cdlemk46  39216  cdlemk47  39217  cdlemk48  39218  cdlemk49  39219  cdlemk50  39220  cdlemk51  39221  cdlemk52  39222  cdlemk55b  39228  cdlemkyyN  39230  cdlemk55u1  39233  cdlemk55u  39234  cdlemk39u1  39235  cdlemk39u  39236  cdlemk56  39239  cdleml3N  39246  cdleml4N  39247  cdlemm10N  39386  dihord1  39486  dihord2a  39487  dihord2b  39488  dihord10  39491  dihord11c  39492  dihord2pre  39493  dihord4  39526  dihord5apre  39530  dihmeetlem1N  39558  dihglbcpreN  39568  dihjatc1  39579  dihjatc3  39581  dihmeetlem13N  39587  dihmeetlem20N  39594  baerlem3lem2  39978  baerlem5alem2  39979  baerlem5blem2  39980  hdmap14lem11  40146  hdmap14lem12  40147  flt4lem5  40749  monotuz  41026  congmul  41052  congsub  41055  rpnnen3lem  41116  ntrclsiso  41998  ntrclskb  42000  ntrclsk3  42001  wessf1ornlem  43049  infleinf  43246  lincdifsn  46116  itsclc0yqe  46458  itsclc0xyqsolr  46466  iscnrm3rlem8  46592  iscnrm3llem2  46595