Theorem simp11 1201

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simp111  1300  simp211  1309  simp311  1318  omeulem1  8375  omeu  8378  ackbij1lem16  9922  coprimeprodsq  16437  pythagtriplem14  16457  pythagtrip  16463  mrelatglb  18193  subglsm  19194  lsmpropd  19198  mdetmul  21680  decpmatid  21827  isfil2  22915  filuni  22944  cxple2a  25759  isosctr  25876  brbtwn2  27176  colinearalg  27181  ax5seglem3  27202  clwwlknonex2  28374  measres  32090  bayesth  32306  nolesgn2o  33801  nolesgn2ores  33802  nogesgn1o  33803  nogesgn1ores  33804  nolt02o  33825  nogt01o  33826  sslttr  33928  cofcut2  34018  ofscom  34236  btwndiff  34256  ifscgr  34273  brofs2  34306  brifs2  34307  fscgr  34309  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem5  34320  btwnconn1lem6  34321  btwnconn1lem7  34322  btwnconn1lem8  34323  btwnconn1lem9  34324  btwnconn1lem10  34325  btwnconn1lem11  34326  btwnconn1lem12  34327  seglecgr12im  34339  seglecgr12  34340  ivthALT  34451  eqlkr  37040  lkrshp  37046  lshpkrlem5  37055  cvrval3  37354  4noncolr3  37394  4noncolr2  37395  4noncolr1  37396  athgt  37397  3dimlem2  37400  3dimlem3a  37401  3dimlem4a  37404  3dimlem4  37405  3dimlem4OLDN  37406  3dim2  37409  1cvratex  37414  hlatexch4  37422  ps-2b  37423  3atlem1  37424  3atlem2  37425  3atlem4  37427  3atlem5  37428  3atlem6  37429  llnnleat  37454  2atm  37468  ps-2c  37469  llnmlplnN  37480  lplnnlelln  37484  2atmat  37502  2llnjN  37508  lvoli2  37522  lvolnlelln  37525  4atlem3b  37539  4atlem9  37544  4atlem10a  37545  4atlem10  37547  4atlem11a  37548  4atlem11b  37549  4atlem12a  37551  4atlem12b  37552  4at  37554  4at2  37555  lplncvrlvol2  37556  2lplnj  37561  dalemswapyz  37597  dath2  37678  lneq2at  37719  2lnat  37725  cdlema1N  37732  cdlemb  37735  paddasslem15  37775  pmodlem1  37787  llnmod2i2  37804  llnexchb2lem  37809  llnexchb2  37810  dalawlem1  37812  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem9  37820  dalawlem10  37821  dalawlem11  37822  dalawlem12  37823  dalawlem13  37824  dalawlem15  37826  dalaw  37827  osumcllem5N  37901  osumcllem6N  37902  osumcllem7N  37903  osumcllem9N  37905  osumcllem10N  37906  osumcllem11N  37907  pl42lem1N  37920  lhpexle3lem  37952  lhpmcvr5N  37968  lhp2atne  37975  lhp2at0ne  37977  4atexlemswapqr  38004  4atexlemex6  38015  ldilco  38057  ltrneq  38090  trlval2  38104  trlnidat  38114  cdlemd2  38140  cdlemd7  38145  cdlemd8  38146  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme11c  38202  cdleme11e  38204  cdleme11l  38210  cdleme11  38211  cdleme14  38214  cdleme15a  38215  cdleme15c  38217  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme0nex  38231  cdleme18d  38236  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20f  38255  cdleme20i  38258  cdleme20k  38260  cdleme20l1  38261  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21a  38266  cdleme21b  38267  cdleme21ct  38270  cdleme21d  38271  cdleme21e  38272  cdleme21f  38273  cdleme21h  38275  cdleme22eALTN  38286  cdleme22f2  38288  cdleme22g  38289  cdleme26e  38300  cdleme26eALTN  38302  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdleme28a  38311  cdleme28b  38312  cdleme28  38314  cdleme29ex  38315  cdleme29c  38317  cdlemefrs29cpre1  38339  cdlemefr29exN  38343  cdlemefr32sn2aw  38345  cdlemefr29bpre0N  38347  cdlemefr29clN  38348  cdlemefr32fvaN  38350  cdlemefr32fva1  38351  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32fva  38378  cdleme32b  38383  cdleme32d  38385  cdleme32e  38386  cdleme32f  38387  cdleme32le  38388  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme35f  38395  cdleme36a  38401  cdleme36m  38402  cdleme37m  38403  cdleme39a  38406  cdleme39n  38407  cdleme40m  38408  cdleme40n  38409  cdleme42e  38420  cdleme42f  38421  cdleme42g  38422  cdleme43bN  38431  cdleme43cN  38432  cdleme43dN  38433  cdleme46f2g2  38434  cdleme46f2g1  38435  cdleme17d2  38436  cdleme48b  38444  cdleme4gfv  38448  cdlemeg49le  38452  cdlemeg46c  38454  cdlemeg46fvaw  38457  cdlemeg46nlpq  38458  cdlemeg46frv  38466  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemeg46gfre  38473  cdleme50trn1  38490  cdleme50trn2a  38491  cdleme50trn2  38492  cdleme  38501  cdlemf  38504  trlord  38510  cdlemg2ce  38533  cdlemg7fvbwN  38548  cdlemg7aN  38566  cdlemg10bALTN  38577  cdlemg10a  38581  cdlemg10  38582  cdlemg12d  38587  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg13  38593  cdlemg17b  38603  cdlemg17dN  38604  cdlemg17dALTN  38605  cdlemg17e  38606  cdlemg17f  38607  cdlemg17g  38608  cdlemg17h  38609  cdlemg17i  38610  cdlemg17pq  38613  cdlemg17bq  38614  cdlemg17iqN  38615  cdlemg17  38618  cdlemg18d  38622  cdlemg18  38623  cdlemg19a  38624  cdlemg19  38625  cdlemg21  38627  cdlemg27a  38633  cdlemg28a  38634  cdlemg31b0N  38635  cdlemg27b  38637  cdlemg33b0  38642  cdlemg28b  38644  cdlemg28  38645  cdlemg33a  38647  cdlemg33  38652  cdlemg34  38653  cdlemg35  38654  cdlemg36  38655  ltrnco  38660  trlcone  38669  cdlemg44  38674  cdlemg47  38677  cdlemg48  38678  tendococl  38713  tendoplcl  38722  cdlemh1  38756  cdlemi  38761  cdlemj1  38762  cdlemj2  38763  tendocan  38765  cdlemk6  38778  cdlemki  38782  cdlemksat  38787  cdlemksv2  38788  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemkoatnle  38792  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk16a  38797  cdlemk16  38798  cdlemk17  38799  cdlemk1u  38800  cdlemk5u  38802  cdlemk6u  38803  cdlemkuat  38807  cdlemk18  38809  cdlemk19  38810  cdlemk12u  38813  cdlemk21N  38814  cdlemk20  38815  cdlemkoatnle-2N  38816  cdlemk13-2N  38817  cdlemkole-2N  38818  cdlemk14-2N  38819  cdlemk15-2N  38820  cdlemk16-2N  38821  cdlemk17-2N  38822  cdlemk18-2N  38827  cdlemk19-2N  38828  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk12u-2N  38831  cdlemk21-2N  38832  cdlemk20-2N  38833  cdlemk22  38834  cdlemk23-3  38843  cdlemk25-3  38845  cdlemk26b-3  38846  cdlemk27-3  38848  cdlemk28-3  38849  cdlemk33N  38850  cdlemk37  38855  cdlemky  38867  cdlemk11ta  38870  cdlemkid3N  38874  cdlemk11tc  38886  cdlemk11t  38887  cdlemk45  38888  cdlemk46  38889  cdlemk47  38890  cdlemk48  38891  cdlemk49  38892  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemk55b  38901  cdlemkyyN  38903  cdlemk55u1  38906  cdlemk55u  38907  cdlemk39u1  38908  cdlemk39u  38909  cdlemk56  38912  cdleml3N  38919  cdleml4N  38920  cdlemm10N  39059  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord10  39164  dihord11c  39165  dihord2pre  39166  dihord4  39199  dihord5apre  39203  dihmeetlem1N  39231  dihglbcpreN  39241  dihjatc1  39252  dihjatc3  39254  dihmeetlem13N  39260  dihmeetlem20N  39267  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  hdmap14lem11  39819  hdmap14lem12  39820  flt4lem5  40403  monotuz  40679  congmul  40705  congsub  40708  rpnnen3lem  40769  ntrclsiso  41566  ntrclskb  41568  ntrclsk3  41569  wessf1ornlem  42611  infleinf  42801  lincdifsn  45653  itsclc0yqe  45995  itsclc0xyqsolr  46003  iscnrm3rlem8  46129  iscnrm3llem2  46132