Theorem simp11 1084

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 1054	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1075	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl11  1129  simpr11  1138  simp111  1183  simp211  1192  simp311  1201  funcnvqpOLD  5867  omeulem1  7549  omeu  7552  ackbij1lem16  8940  coprimeprodsq  15351  pythagtriplem14  15371  pythagtrip  15377  mrelatglb  17007  subglsm  17909  lsmpropd  17913  mdetmul  20248  decpmatid  20394  isfil2  21470  filuni  21499  cxple2a  24245  isosctr  24351  brbtwn2  25585  colinearalg  25590  ax5seglem3  25611  numclwwlkovf2ex  26613  measres  29612  bayesth  29828  ofscom  31284  btwndiff  31304  ifscgr  31321  brofs2  31354  brifs2  31355  fscgr  31357  btwnconn1lem1  31364  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem7  31370  btwnconn1lem8  31371  btwnconn1lem9  31372  btwnconn1lem10  31373  btwnconn1lem11  31374  btwnconn1lem12  31375  seglecgr12im  31387  seglecgr12  31388  ivthALT  31500  eqlkr  33404  lkrshp  33410  lshpkrlem5  33419  cvrval3  33717  4noncolr3  33757  4noncolr2  33758  4noncolr1  33759  athgt  33760  3dimlem2  33763  3dimlem3a  33764  3dimlem4a  33767  3dimlem4  33768  3dimlem4OLDN  33769  3dim2  33772  1cvratex  33777  hlatexch4  33785  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem4  33790  3atlem5  33791  3atlem6  33792  llnnleat  33817  2atm  33831  ps-2c  33832  llnmlplnN  33843  lplnnlelln  33847  2atmat  33865  2llnjN  33871  lvoli2  33885  lvolnlelln  33888  4atlem3b  33902  4atlem9  33907  4atlem10a  33908  4atlem10  33910  4atlem11a  33911  4atlem11b  33912  4atlem12a  33914  4atlem12b  33915  4at  33917  4at2  33918  lplncvrlvol2  33919  2lplnj  33924  dalemswapyz  33960  dath2  34041  lneq2at  34082  2lnat  34088  cdlema1N  34095  cdlemb  34098  paddasslem15  34138  pmodlem1  34150  llnmod2i2  34167  llnexchb2lem  34172  llnexchb2  34173  dalawlem1  34175  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem10  34184  dalawlem11  34185  dalawlem12  34186  dalawlem13  34187  dalawlem15  34189  dalaw  34190  osumcllem5N  34264  osumcllem6N  34265  osumcllem7N  34266  osumcllem9N  34268  osumcllem10N  34269  osumcllem11N  34270  pl42lem1N  34283  lhpexle3lem  34315  lhpmcvr5N  34331  lhp2atne  34338  lhp2at0ne  34340  4atexlemswapqr  34367  4atexlemex6  34378  ldilco  34420  ltrneq  34453  trlval2  34468  trlnidat  34478  cdlemd2  34504  cdlemd7  34509  cdlemd8  34510  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme11c  34566  cdleme11e  34568  cdleme11l  34574  cdleme11  34575  cdleme14  34578  cdleme15a  34579  cdleme15c  34581  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme0nex  34595  cdleme18d  34600  cdleme19b  34610  cdleme19d  34612  cdleme19e  34613  cdleme20f  34620  cdleme20i  34623  cdleme20k  34625  cdleme20l1  34626  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21a  34631  cdleme21b  34632  cdleme21ct  34635  cdleme21d  34636  cdleme21e  34637  cdleme21f  34638  cdleme21h  34640  cdleme22eALTN  34651  cdleme22f2  34653  cdleme22g  34654  cdleme26e  34665  cdleme26eALTN  34667  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme28a  34676  cdleme28b  34677  cdleme28  34679  cdleme29ex  34680  cdleme29c  34682  cdlemefrs29cpre1  34704  cdlemefr29exN  34708  cdlemefr32sn2aw  34710  cdlemefr29bpre0N  34712  cdlemefr29clN  34713  cdlemefr32fvaN  34715  cdlemefr32fva1  34716  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme41sn3a  34739  cdleme32fva  34743  cdleme32b  34748  cdleme32d  34750  cdleme32e  34751  cdleme32f  34752  cdleme32le  34753  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35e  34759  cdleme35f  34760  cdleme36a  34766  cdleme36m  34767  cdleme37m  34768  cdleme39a  34771  cdleme39n  34772  cdleme40m  34773  cdleme40n  34774  cdleme42e  34785  cdleme42f  34786  cdleme42g  34787  cdleme43bN  34796  cdleme43cN  34797  cdleme43dN  34798  cdleme46f2g2  34799  cdleme46f2g1  34800  cdleme17d2  34801  cdleme48b  34809  cdleme4gfv  34813  cdlemeg49le  34817  cdlemeg46c  34819  cdlemeg46fvaw  34822  cdlemeg46nlpq  34823  cdlemeg46frv  34831  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemeg46gfre  34838  cdleme50trn1  34855  cdleme50trn2a  34856  cdleme50trn2  34857  cdleme  34866  cdlemf  34869  trlord  34875  cdlemg2ce  34898  cdlemg7fvbwN  34913  cdlemg7aN  34931  cdlemg10bALTN  34942  cdlemg10a  34946  cdlemg10  34947  cdlemg12d  34952  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg13  34958  cdlemg17b  34968  cdlemg17dN  34969  cdlemg17dALTN  34970  cdlemg17e  34971  cdlemg17f  34972  cdlemg17g  34973  cdlemg17h  34974  cdlemg17i  34975  cdlemg17pq  34978  cdlemg17bq  34979  cdlemg17iqN  34980  cdlemg17  34983  cdlemg18d  34987  cdlemg18  34988  cdlemg19a  34989  cdlemg19  34990  cdlemg21  34992  cdlemg27a  34998  cdlemg28a  34999  cdlemg31b0N  35000  cdlemg27b  35002  cdlemg33b0  35007  cdlemg28b  35009  cdlemg28  35010  cdlemg33a  35012  cdlemg33  35017  cdlemg34  35018  cdlemg35  35019  cdlemg36  35020  ltrnco  35025  trlcone  35034  cdlemg44  35039  cdlemg47  35042  cdlemg48  35043  tendococl  35078  tendoplcl  35087  cdlemh1  35121  cdlemi  35126  cdlemj1  35127  cdlemj2  35128  tendocan  35130  cdlemk6  35143  cdlemki  35147  cdlemksat  35152  cdlemksv2  35153  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemkoatnle  35157  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk16a  35162  cdlemk16  35163  cdlemk17  35164  cdlemk1u  35165  cdlemk5u  35167  cdlemk6u  35168  cdlemkuat  35172  cdlemk18  35174  cdlemk19  35175  cdlemk12u  35178  cdlemk21N  35179  cdlemk20  35180  cdlemkoatnle-2N  35181  cdlemk13-2N  35182  cdlemkole-2N  35183  cdlemk14-2N  35184  cdlemk15-2N  35185  cdlemk16-2N  35186  cdlemk17-2N  35187  cdlemk18-2N  35192  cdlemk19-2N  35193  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk21-2N  35197  cdlemk20-2N  35198  cdlemk22  35199  cdlemk23-3  35208  cdlemk25-3  35210  cdlemk26b-3  35211  cdlemk27-3  35213  cdlemk28-3  35214  cdlemk33N  35215  cdlemk37  35220  cdlemky  35232  cdlemk11ta  35235  cdlemkid3N  35239  cdlemk11tc  35251  cdlemk11t  35252  cdlemk45  35253  cdlemk46  35254  cdlemk47  35255  cdlemk48  35256  cdlemk49  35257  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  cdlemk55b  35266  cdlemkyyN  35268  cdlemk55u1  35271  cdlemk55u  35272  cdlemk39u1  35273  cdlemk39u  35274  cdlemk56  35277  cdleml3N  35284  cdleml4N  35285  cdlemm10N  35425  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord10  35530  dihord11c  35531  dihord2pre  35532  dihord4  35565  dihord5apre  35569  dihmeetlem1N  35597  dihglbcpreN  35607  dihjatc1  35618  dihjatc3  35620  dihmeetlem13N  35626  dihmeetlem20N  35633  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  hdmap14lem11  36188  hdmap14lem12  36189  monotuz  36524  congmul  36552  congsub  36555  rpnnen3lem  36616  ntrclsiso  37385  ntrclskb  37387  ntrclsk3  37388  wessf1ornlem  38366  infleinf  38529  av-numclwwlkovf2ex  41517  lincdifsn  42007