Theorem simp11 1222

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp111  1321  simp211  1330  simp311  1339  omeulem1  8574  omeu  8577  ackbij1lem16  10293  coprimeprodsq  16966  pythagtriplem14  16986  pythagtrip  16992  mrelatglb  18714  subglsm  19867  lsmpropd  19871  mdetmul  22918  decpmatid  23068  isfil2  24155  filuni  24184  cxple2a  27009  isosctr  27131  flt4lem5  27962  nolesgn2o  28010  nolesgn2ores  28011  nogesgn1o  28012  nogesgn1ores  28013  nolt02o  28034  nogt01o  28035  sltstr  28155  cofcut2  28290  brbtwn2  29465  colinearalg  29470  ax5seglem3  29491  clwwlknonex2  30682  measres  34837  bayesth  35054  ofscom  36742  btwndiff  36762  ifscgr  36779  brofs2  36812  brifs2  36813  fscgr  36815  btwnconn1lem1  36822  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem5  36826  btwnconn1lem6  36827  btwnconn1lem7  36828  btwnconn1lem8  36829  btwnconn1lem9  36830  btwnconn1lem10  36831  btwnconn1lem11  36832  btwnconn1lem12  36833  seglecgr12im  36845  seglecgr12  36846  ivthALT  37093  eqlkr  40124  lkrshp  40130  lshpkrlem5  40139  cvrval3  40438  4noncolr3  40478  4noncolr2  40479  4noncolr1  40480  athgt  40481  3dimlem2  40484  3dimlem3a  40485  3dimlem4a  40488  3dimlem4  40489  3dimlem4OLDN  40490  3dim2  40493  1cvratex  40498  hlatexch4  40506  ps-2b  40507  3atlem1  40508  3atlem2  40509  3atlem4  40511  3atlem5  40512  3atlem6  40513  llnnleat  40538  2atm  40552  ps-2c  40553  llnmlplnN  40564  lplnnlelln  40568  2atmat  40586  2llnjN  40592  lvoli2  40606  lvolnlelln  40609  4atlem3b  40623  4atlem9  40628  4atlem10a  40629  4atlem10  40631  4atlem11a  40632  4atlem11b  40633  4atlem12a  40635  4atlem12b  40636  4at  40638  4at2  40639  lplncvrlvol2  40640  2lplnj  40645  dalemswapyz  40681  dath2  40762  lneq2at  40803  2lnat  40809  cdlema1N  40816  cdlemb  40819  paddasslem15  40859  pmodlem1  40871  llnmod2i2  40888  llnexchb2lem  40893  llnexchb2  40894  dalawlem1  40896  dalawlem3  40898  dalawlem4  40899  dalawlem5  40900  dalawlem6  40901  dalawlem7  40902  dalawlem8  40903  dalawlem9  40904  dalawlem10  40905  dalawlem11  40906  dalawlem12  40907  dalawlem13  40908  dalawlem15  40910  dalaw  40911  osumcllem5N  40985  osumcllem6N  40986  osumcllem7N  40987  osumcllem9N  40989  osumcllem10N  40990  osumcllem11N  40991  pl42lem1N  41004  lhpexle3lem  41036  lhpmcvr5N  41052  lhp2atne  41059  lhp2at0ne  41061  4atexlemswapqr  41088  4atexlemex6  41099  ldilco  41141  ltrneq  41174  trlval2  41188  trlnidat  41198  cdlemd2  41224  cdlemd7  41229  cdlemd8  41230  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme11c  41286  cdleme11e  41288  cdleme11l  41294  cdleme11  41295  cdleme14  41298  cdleme15a  41299  cdleme15c  41301  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme16e  41307  cdleme16f  41308  cdleme0nex  41315  cdleme18d  41320  cdleme19b  41329  cdleme19d  41331  cdleme19e  41332  cdleme20f  41339  cdleme20i  41342  cdleme20k  41344  cdleme20l1  41345  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme21a  41350  cdleme21b  41351  cdleme21ct  41354  cdleme21d  41355  cdleme21e  41356  cdleme21f  41357  cdleme21h  41359  cdleme22eALTN  41370  cdleme22f2  41372  cdleme22g  41373  cdleme26e  41384  cdleme26eALTN  41386  cdleme26fALTN  41387  cdleme26f  41388  cdleme26f2ALTN  41389  cdleme26f2  41390  cdleme28a  41395  cdleme28b  41396  cdleme28  41398  cdleme29ex  41399  cdleme29c  41401  cdlemefrs29cpre1  41423  cdlemefr29exN  41427  cdlemefr32sn2aw  41429  cdlemefr29bpre0N  41431  cdlemefr29clN  41432  cdlemefr32fvaN  41434  cdlemefr32fva1  41435  cdlemefs32sn1aw  41439  cdleme43fsv1snlem  41445  cdleme41sn3a  41458  cdleme32fva  41462  cdleme32b  41467  cdleme32d  41469  cdleme32e  41470  cdleme32f  41471  cdleme32le  41472  cdleme35a  41473  cdleme35fnpq  41474  cdleme35b  41475  cdleme35c  41476  cdleme35d  41477  cdleme35e  41478  cdleme35f  41479  cdleme36a  41485  cdleme36m  41486  cdleme37m  41487  cdleme39a  41490  cdleme39n  41491  cdleme40m  41492  cdleme40n  41493  cdleme42e  41504  cdleme42f  41505  cdleme42g  41506  cdleme43bN  41515  cdleme43cN  41516  cdleme43dN  41517  cdleme46f2g2  41518  cdleme46f2g1  41519  cdleme17d2  41520  cdleme48b  41528  cdleme4gfv  41532  cdlemeg49le  41536  cdlemeg46c  41538  cdlemeg46fvaw  41541  cdlemeg46nlpq  41542  cdlemeg46frv  41550  cdlemeg46rgv  41553  cdlemeg46req  41554  cdlemeg46gfre  41557  cdleme50trn1  41574  cdleme50trn2a  41575  cdleme50trn2  41576  cdleme  41585  cdlemf  41588  trlord  41594  cdlemg2ce  41617  cdlemg7fvbwN  41632  cdlemg7aN  41650  cdlemg10bALTN  41661  cdlemg10a  41665  cdlemg10  41666  cdlemg12d  41671  cdlemg12f  41673  cdlemg12g  41674  cdlemg12  41675  cdlemg13a  41676  cdlemg13  41677  cdlemg17b  41687  cdlemg17dN  41688  cdlemg17dALTN  41689  cdlemg17e  41690  cdlemg17f  41691  cdlemg17g  41692  cdlemg17h  41693  cdlemg17i  41694  cdlemg17pq  41697  cdlemg17bq  41698  cdlemg17iqN  41699  cdlemg17  41702  cdlemg18d  41706  cdlemg18  41707  cdlemg19a  41708  cdlemg19  41709  cdlemg21  41711  cdlemg27a  41717  cdlemg28a  41718  cdlemg31b0N  41719  cdlemg27b  41721  cdlemg33b0  41726  cdlemg28b  41728  cdlemg28  41729  cdlemg33a  41731  cdlemg33  41736  cdlemg34  41737  cdlemg35  41738  cdlemg36  41739  ltrnco  41744  trlcone  41753  cdlemg44  41758  cdlemg47  41761  cdlemg48  41762  tendococl  41797  tendoplcl  41806  cdlemh1  41840  cdlemi  41845  cdlemj1  41846  cdlemj2  41847  tendocan  41849  cdlemk6  41862  cdlemki  41866  cdlemksat  41871  cdlemksv2  41872  cdlemk7  41873  cdlemk11  41874  cdlemk12  41875  cdlemkoatnle  41876  cdlemkole  41878  cdlemk14  41879  cdlemk15  41880  cdlemk16a  41881  cdlemk16  41882  cdlemk17  41883  cdlemk1u  41884  cdlemk5u  41886  cdlemk6u  41887  cdlemkuat  41891  cdlemk18  41893  cdlemk19  41894  cdlemk12u  41897  cdlemk21N  41898  cdlemk20  41899  cdlemkoatnle-2N  41900  cdlemk13-2N  41901  cdlemkole-2N  41902  cdlemk14-2N  41903  cdlemk15-2N  41904  cdlemk16-2N  41905  cdlemk17-2N  41906  cdlemk18-2N  41911  cdlemk19-2N  41912  cdlemk7u-2N  41913  cdlemk11u-2N  41914  cdlemk12u-2N  41915  cdlemk21-2N  41916  cdlemk20-2N  41917  cdlemk22  41918  cdlemk23-3  41927  cdlemk25-3  41929  cdlemk26b-3  41930  cdlemk27-3  41932  cdlemk28-3  41933  cdlemk33N  41934  cdlemk37  41939  cdlemky  41951  cdlemk11ta  41954  cdlemkid3N  41958  cdlemk11tc  41970  cdlemk11t  41971  cdlemk45  41972  cdlemk46  41973  cdlemk47  41974  cdlemk48  41975  cdlemk49  41976  cdlemk50  41977  cdlemk51  41978  cdlemk52  41979  cdlemk55b  41985  cdlemkyyN  41987  cdlemk55u1  41990  cdlemk55u  41991  cdlemk39u1  41992  cdlemk39u  41993  cdlemk56  41996  cdleml3N  42003  cdleml4N  42004  cdlemm10N  42143  dihord1  42243  dihord2a  42244  dihord2b  42245  dihord10  42248  dihord11c  42249  dihord2pre  42250  dihord4  42283  dihord5apre  42287  dihmeetlem1N  42315  dihglbcpreN  42325  dihjatc1  42336  dihjatc3  42338  dihmeetlem13N  42344  dihmeetlem20N  42351  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  hdmap14lem11  42903  hdmap14lem12  42904  monotuz  43901  congmul  43927  congsub  43930  rpnnen3lem  43991  ntrclsiso  45026  ntrclskb  45028  ntrclsk3  45029  wessf1ornlem  46143  infleinf  46327  lincdifsn  49480  itsclc0yqe  49817  itsclc0xyqsolr  49825  iscnrm3rlem8  49999  iscnrm3llem2  50002