Theorem simp11 1205

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

Syntax hints:   → wi 4   ∧ w3a 1087

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

This theorem is referenced by:  simp111  1304  simp211  1313  simp311  1322  omeulem1  8510  omeu  8513  ackbij1lem16  10147  coprimeprodsq  16770  pythagtriplem14  16790  pythagtrip  16796  mrelatglb  18517  subglsm  19639  lsmpropd  19643  mdetmul  22598  decpmatid  22745  isfil2  23831  filuni  23860  cxple2a  26676  isosctr  26798  nolesgn2o  27649  nolesgn2ores  27650  nogesgn1o  27651  nogesgn1ores  27652  nolt02o  27673  nogt01o  27674  sltstr  27793  cofcut2  27928  brbtwn2  28988  colinearalg  28993  ax5seglem3  29014  clwwlknonex2  30194  measres  34382  bayesth  34599  ofscom  36205  btwndiff  36225  ifscgr  36242  brofs2  36275  brifs2  36276  fscgr  36278  btwnconn1lem1  36285  btwnconn1lem2  36286  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem7  36291  btwnconn1lem8  36292  btwnconn1lem9  36293  btwnconn1lem10  36294  btwnconn1lem11  36295  btwnconn1lem12  36296  seglecgr12im  36308  seglecgr12  36309  ivthALT  36533  eqlkr  39559  lkrshp  39565  lshpkrlem5  39574  cvrval3  39873  4noncolr3  39913  4noncolr2  39914  4noncolr1  39915  athgt  39916  3dimlem2  39919  3dimlem3a  39920  3dimlem4a  39923  3dimlem4  39924  3dimlem4OLDN  39925  3dim2  39928  1cvratex  39933  hlatexch4  39941  ps-2b  39942  3atlem1  39943  3atlem2  39944  3atlem4  39946  3atlem5  39947  3atlem6  39948  llnnleat  39973  2atm  39987  ps-2c  39988  llnmlplnN  39999  lplnnlelln  40003  2atmat  40021  2llnjN  40027  lvoli2  40041  lvolnlelln  40044  4atlem3b  40058  4atlem9  40063  4atlem10a  40064  4atlem10  40066  4atlem11a  40067  4atlem11b  40068  4atlem12a  40070  4atlem12b  40071  4at  40073  4at2  40074  lplncvrlvol2  40075  2lplnj  40080  dalemswapyz  40116  dath2  40197  lneq2at  40238  2lnat  40244  cdlema1N  40251  cdlemb  40254  paddasslem15  40294  pmodlem1  40306  llnmod2i2  40323  llnexchb2lem  40328  llnexchb2  40329  dalawlem1  40331  dalawlem3  40333  dalawlem4  40334  dalawlem5  40335  dalawlem6  40336  dalawlem7  40337  dalawlem8  40338  dalawlem9  40339  dalawlem10  40340  dalawlem11  40341  dalawlem12  40342  dalawlem13  40343  dalawlem15  40345  dalaw  40346  osumcllem5N  40420  osumcllem6N  40421  osumcllem7N  40422  osumcllem9N  40424  osumcllem10N  40425  osumcllem11N  40426  pl42lem1N  40439  lhpexle3lem  40471  lhpmcvr5N  40487  lhp2atne  40494  lhp2at0ne  40496  4atexlemswapqr  40523  4atexlemex6  40534  ldilco  40576  ltrneq  40609  trlval2  40623  trlnidat  40633  cdlemd2  40659  cdlemd7  40664  cdlemd8  40665  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme11c  40721  cdleme11e  40723  cdleme11l  40729  cdleme11  40730  cdleme14  40733  cdleme15a  40734  cdleme15c  40736  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme0nex  40750  cdleme18d  40755  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20f  40774  cdleme20i  40777  cdleme20k  40779  cdleme20l1  40780  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21a  40785  cdleme21b  40786  cdleme21ct  40789  cdleme21d  40790  cdleme21e  40791  cdleme21f  40792  cdleme21h  40794  cdleme22eALTN  40805  cdleme22f2  40807  cdleme22g  40808  cdleme26e  40819  cdleme26eALTN  40821  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme28a  40830  cdleme28b  40831  cdleme28  40833  cdleme29ex  40834  cdleme29c  40836  cdlemefrs29cpre1  40858  cdlemefr29exN  40862  cdlemefr32sn2aw  40864  cdlemefr29bpre0N  40866  cdlemefr29clN  40867  cdlemefr32fvaN  40869  cdlemefr32fva1  40870  cdlemefs32sn1aw  40874  cdleme43fsv1snlem  40880  cdleme41sn3a  40893  cdleme32fva  40897  cdleme32b  40902  cdleme32d  40904  cdleme32e  40905  cdleme32f  40906  cdleme32le  40907  cdleme35a  40908  cdleme35fnpq  40909  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35e  40913  cdleme35f  40914  cdleme36a  40920  cdleme36m  40921  cdleme37m  40922  cdleme39a  40925  cdleme39n  40926  cdleme40m  40927  cdleme40n  40928  cdleme42e  40939  cdleme42f  40940  cdleme42g  40941  cdleme43bN  40950  cdleme43cN  40951  cdleme43dN  40952  cdleme46f2g2  40953  cdleme46f2g1  40954  cdleme17d2  40955  cdleme48b  40963  cdleme4gfv  40967  cdlemeg49le  40971  cdlemeg46c  40973  cdlemeg46fvaw  40976  cdlemeg46nlpq  40977  cdlemeg46frv  40985  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfre  40992  cdleme50trn1  41009  cdleme50trn2a  41010  cdleme50trn2  41011  cdleme  41020  cdlemf  41023  trlord  41029  cdlemg2ce  41052  cdlemg7fvbwN  41067  cdlemg7aN  41085  cdlemg10bALTN  41096  cdlemg10a  41100  cdlemg10  41101  cdlemg12d  41106  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg13a  41111  cdlemg13  41112  cdlemg17b  41122  cdlemg17dN  41123  cdlemg17dALTN  41124  cdlemg17e  41125  cdlemg17f  41126  cdlemg17g  41127  cdlemg17h  41128  cdlemg17i  41129  cdlemg17pq  41132  cdlemg17bq  41133  cdlemg17iqN  41134  cdlemg17  41137  cdlemg18d  41141  cdlemg18  41142  cdlemg19a  41143  cdlemg19  41144  cdlemg21  41146  cdlemg27a  41152  cdlemg28a  41153  cdlemg31b0N  41154  cdlemg27b  41156  cdlemg33b0  41161  cdlemg28b  41163  cdlemg28  41164  cdlemg33a  41166  cdlemg33  41171  cdlemg34  41172  cdlemg35  41173  cdlemg36  41174  ltrnco  41179  trlcone  41188  cdlemg44  41193  cdlemg47  41196  cdlemg48  41197  tendococl  41232  tendoplcl  41241  cdlemh1  41275  cdlemi  41280  cdlemj1  41281  cdlemj2  41282  tendocan  41284  cdlemk6  41297  cdlemki  41301  cdlemksat  41306  cdlemksv2  41307  cdlemk7  41308  cdlemk11  41309  cdlemk12  41310  cdlemkoatnle  41311  cdlemkole  41313  cdlemk14  41314  cdlemk15  41315  cdlemk16a  41316  cdlemk16  41317  cdlemk17  41318  cdlemk1u  41319  cdlemk5u  41321  cdlemk6u  41322  cdlemkuat  41326  cdlemk18  41328  cdlemk19  41329  cdlemk12u  41332  cdlemk21N  41333  cdlemk20  41334  cdlemkoatnle-2N  41335  cdlemk13-2N  41336  cdlemkole-2N  41337  cdlemk14-2N  41338  cdlemk15-2N  41339  cdlemk16-2N  41340  cdlemk17-2N  41341  cdlemk18-2N  41346  cdlemk19-2N  41347  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk12u-2N  41350  cdlemk21-2N  41351  cdlemk20-2N  41352  cdlemk22  41353  cdlemk23-3  41362  cdlemk25-3  41364  cdlemk26b-3  41365  cdlemk27-3  41367  cdlemk28-3  41368  cdlemk33N  41369  cdlemk37  41374  cdlemky  41386  cdlemk11ta  41389  cdlemkid3N  41393  cdlemk11tc  41405  cdlemk11t  41406  cdlemk45  41407  cdlemk46  41408  cdlemk47  41409  cdlemk48  41410  cdlemk49  41411  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemk55b  41420  cdlemkyyN  41422  cdlemk55u1  41425  cdlemk55u  41426  cdlemk39u1  41427  cdlemk39u  41428  cdlemk56  41431  cdleml3N  41438  cdleml4N  41439  cdlemm10N  41578  dihord1  41678  dihord2a  41679  dihord2b  41680  dihord10  41683  dihord11c  41684  dihord2pre  41685  dihord4  41718  dihord5apre  41722  dihmeetlem1N  41750  dihglbcpreN  41760  dihjatc1  41771  dihjatc3  41773  dihmeetlem13N  41779  dihmeetlem20N  41786  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  hdmap14lem11  42338  hdmap14lem12  42339  flt4lem5  43097  monotuz  43387  congmul  43413  congsub  43416  rpnnen3lem  43477  ntrclsiso  44512  ntrclskb  44514  ntrclsk3  44515  wessf1ornlem  45633  infleinf  45819  lincdifsn  48912  itsclc0yqe  49249  itsclc0xyqsolr  49257  iscnrm3rlem8  49434  iscnrm3llem2  49437