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 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp111  1321  simp211  1330  simp311  1339  omeulem1  8568  omeu  8571  ackbij1lem16  10218  coprimeprodsq  16869  pythagtriplem14  16889  pythagtrip  16895  mrelatglb  18617  subglsm  19744  lsmpropd  19748  mdetmul  22761  decpmatid  22908  isfil2  23994  filuni  24023  cxple2a  26845  isosctr  26967  nolesgn2o  27816  nolesgn2ores  27817  nogesgn1o  27818  nogesgn1ores  27819  nolt02o  27840  nogt01o  27841  sltstr  27961  cofcut2  28096  brbtwn2  29236  colinearalg  29241  ax5seglem3  29262  clwwlknonex2  30441  measres  34593  bayesth  34810  ofscom  36480  btwndiff  36500  ifscgr  36517  brofs2  36550  brifs2  36551  fscgr  36553  btwnconn1lem1  36560  btwnconn1lem2  36561  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem5  36564  btwnconn1lem6  36565  btwnconn1lem7  36566  btwnconn1lem8  36567  btwnconn1lem9  36568  btwnconn1lem10  36569  btwnconn1lem11  36570  btwnconn1lem12  36571  seglecgr12im  36583  seglecgr12  36584  ivthALT  36827  eqlkr  39854  lkrshp  39860  lshpkrlem5  39869  cvrval3  40168  4noncolr3  40208  4noncolr2  40209  4noncolr1  40210  athgt  40211  3dimlem2  40214  3dimlem3a  40215  3dimlem4a  40218  3dimlem4  40219  3dimlem4OLDN  40220  3dim2  40223  1cvratex  40228  hlatexch4  40236  ps-2b  40237  3atlem1  40238  3atlem2  40239  3atlem4  40241  3atlem5  40242  3atlem6  40243  llnnleat  40268  2atm  40282  ps-2c  40283  llnmlplnN  40294  lplnnlelln  40298  2atmat  40316  2llnjN  40322  lvoli2  40336  lvolnlelln  40339  4atlem3b  40353  4atlem9  40358  4atlem10a  40359  4atlem10  40361  4atlem11a  40362  4atlem11b  40363  4atlem12a  40365  4atlem12b  40366  4at  40368  4at2  40369  lplncvrlvol2  40370  2lplnj  40375  dalemswapyz  40411  dath2  40492  lneq2at  40533  2lnat  40539  cdlema1N  40546  cdlemb  40549  paddasslem15  40589  pmodlem1  40601  llnmod2i2  40618  llnexchb2lem  40623  llnexchb2  40624  dalawlem1  40626  dalawlem3  40628  dalawlem4  40629  dalawlem5  40630  dalawlem6  40631  dalawlem7  40632  dalawlem8  40633  dalawlem9  40634  dalawlem10  40635  dalawlem11  40636  dalawlem12  40637  dalawlem13  40638  dalawlem15  40640  dalaw  40641  osumcllem5N  40715  osumcllem6N  40716  osumcllem7N  40717  osumcllem9N  40719  osumcllem10N  40720  osumcllem11N  40721  pl42lem1N  40734  lhpexle3lem  40766  lhpmcvr5N  40782  lhp2atne  40789  lhp2at0ne  40791  4atexlemswapqr  40818  4atexlemex6  40829  ldilco  40871  ltrneq  40904  trlval2  40918  trlnidat  40928  cdlemd2  40954  cdlemd7  40959  cdlemd8  40960  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme11c  41016  cdleme11e  41018  cdleme11l  41024  cdleme11  41025  cdleme14  41028  cdleme15a  41029  cdleme15c  41031  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme0nex  41045  cdleme18d  41050  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20f  41069  cdleme20i  41072  cdleme20k  41074  cdleme20l1  41075  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme21a  41080  cdleme21b  41081  cdleme21ct  41084  cdleme21d  41085  cdleme21e  41086  cdleme21f  41087  cdleme21h  41089  cdleme22eALTN  41100  cdleme22f2  41102  cdleme22g  41103  cdleme26e  41114  cdleme26eALTN  41116  cdleme26fALTN  41117  cdleme26f  41118  cdleme26f2ALTN  41119  cdleme26f2  41120  cdleme28a  41125  cdleme28b  41126  cdleme28  41128  cdleme29ex  41129  cdleme29c  41131  cdlemefrs29cpre1  41153  cdlemefr29exN  41157  cdlemefr32sn2aw  41159  cdlemefr29bpre0N  41161  cdlemefr29clN  41162  cdlemefr32fvaN  41164  cdlemefr32fva1  41165  cdlemefs32sn1aw  41169  cdleme43fsv1snlem  41175  cdleme41sn3a  41188  cdleme32fva  41192  cdleme32b  41197  cdleme32d  41199  cdleme32e  41200  cdleme32f  41201  cdleme32le  41202  cdleme35a  41203  cdleme35fnpq  41204  cdleme35b  41205  cdleme35c  41206  cdleme35d  41207  cdleme35e  41208  cdleme35f  41209  cdleme36a  41215  cdleme36m  41216  cdleme37m  41217  cdleme39a  41220  cdleme39n  41221  cdleme40m  41222  cdleme40n  41223  cdleme42e  41234  cdleme42f  41235  cdleme42g  41236  cdleme43bN  41245  cdleme43cN  41246  cdleme43dN  41247  cdleme46f2g2  41248  cdleme46f2g1  41249  cdleme17d2  41250  cdleme48b  41258  cdleme4gfv  41262  cdlemeg49le  41266  cdlemeg46c  41268  cdlemeg46fvaw  41271  cdlemeg46nlpq  41272  cdlemeg46frv  41280  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemeg46gfre  41287  cdleme50trn1  41304  cdleme50trn2a  41305  cdleme50trn2  41306  cdleme  41315  cdlemf  41318  trlord  41324  cdlemg2ce  41347  cdlemg7fvbwN  41362  cdlemg7aN  41380  cdlemg10bALTN  41391  cdlemg10a  41395  cdlemg10  41396  cdlemg12d  41401  cdlemg12f  41403  cdlemg12g  41404  cdlemg12  41405  cdlemg13a  41406  cdlemg13  41407  cdlemg17b  41417  cdlemg17dN  41418  cdlemg17dALTN  41419  cdlemg17e  41420  cdlemg17f  41421  cdlemg17g  41422  cdlemg17h  41423  cdlemg17i  41424  cdlemg17pq  41427  cdlemg17bq  41428  cdlemg17iqN  41429  cdlemg17  41432  cdlemg18d  41436  cdlemg18  41437  cdlemg19a  41438  cdlemg19  41439  cdlemg21  41441  cdlemg27a  41447  cdlemg28a  41448  cdlemg31b0N  41449  cdlemg27b  41451  cdlemg33b0  41456  cdlemg28b  41458  cdlemg28  41459  cdlemg33a  41461  cdlemg33  41466  cdlemg34  41467  cdlemg35  41468  cdlemg36  41469  ltrnco  41474  trlcone  41483  cdlemg44  41488  cdlemg47  41491  cdlemg48  41492  tendococl  41527  tendoplcl  41536  cdlemh1  41570  cdlemi  41575  cdlemj1  41576  cdlemj2  41577  tendocan  41579  cdlemk6  41592  cdlemki  41596  cdlemksat  41601  cdlemksv2  41602  cdlemk7  41603  cdlemk11  41604  cdlemk12  41605  cdlemkoatnle  41606  cdlemkole  41608  cdlemk14  41609  cdlemk15  41610  cdlemk16a  41611  cdlemk16  41612  cdlemk17  41613  cdlemk1u  41614  cdlemk5u  41616  cdlemk6u  41617  cdlemkuat  41621  cdlemk18  41623  cdlemk19  41624  cdlemk12u  41627  cdlemk21N  41628  cdlemk20  41629  cdlemkoatnle-2N  41630  cdlemk13-2N  41631  cdlemkole-2N  41632  cdlemk14-2N  41633  cdlemk15-2N  41634  cdlemk16-2N  41635  cdlemk17-2N  41636  cdlemk18-2N  41641  cdlemk19-2N  41642  cdlemk7u-2N  41643  cdlemk11u-2N  41644  cdlemk12u-2N  41645  cdlemk21-2N  41646  cdlemk20-2N  41647  cdlemk22  41648  cdlemk23-3  41657  cdlemk25-3  41659  cdlemk26b-3  41660  cdlemk27-3  41662  cdlemk28-3  41663  cdlemk33N  41664  cdlemk37  41669  cdlemky  41681  cdlemk11ta  41684  cdlemkid3N  41688  cdlemk11tc  41700  cdlemk11t  41701  cdlemk45  41702  cdlemk46  41703  cdlemk47  41704  cdlemk48  41705  cdlemk49  41706  cdlemk50  41707  cdlemk51  41708  cdlemk52  41709  cdlemk55b  41715  cdlemkyyN  41717  cdlemk55u1  41720  cdlemk55u  41721  cdlemk39u1  41722  cdlemk39u  41723  cdlemk56  41726  cdleml3N  41733  cdleml4N  41734  cdlemm10N  41873  dihord1  41973  dihord2a  41974  dihord2b  41975  dihord10  41978  dihord11c  41979  dihord2pre  41980  dihord4  42013  dihord5apre  42017  dihmeetlem1N  42045  dihglbcpreN  42055  dihjatc1  42066  dihjatc3  42068  dihmeetlem13N  42074  dihmeetlem20N  42081  baerlem3lem2  42465  baerlem5alem2  42466  baerlem5blem2  42467  hdmap14lem11  42633  hdmap14lem12  42634  flt4lem5  43365  monotuz  43651  congmul  43677  congsub  43680  rpnnen3lem  43741  ntrclsiso  44776  ntrclskb  44778  ntrclsk3  44779  wessf1ornlem  45886  infleinf  46070  lincdifsn  49187  itsclc0yqe  49524  itsclc0xyqsolr  49532  iscnrm3rlem8  49708  iscnrm3llem2  49711