Theorem simp11 1220

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  simp111  1319  simp211  1328  simp311  1337  omeulem1  8555  omeu  8558  ackbij1lem16  10205  coprimeprodsq  16858  pythagtriplem14  16878  pythagtrip  16884  mrelatglb  18606  subglsm  19734  lsmpropd  19738  mdetmul  22741  decpmatid  22888  isfil2  23974  filuni  24003  cxple2a  26822  isosctr  26944  nolesgn2o  27793  nolesgn2ores  27794  nogesgn1o  27795  nogesgn1ores  27796  nolt02o  27817  nogt01o  27818  sltstr  27938  cofcut2  28073  brbtwn2  29164  colinearalg  29169  ax5seglem3  29190  clwwlknonex2  30369  measres  34529  bayesth  34746  ofscom  36370  btwndiff  36390  ifscgr  36407  brofs2  36440  brifs2  36441  fscgr  36443  btwnconn1lem1  36450  btwnconn1lem2  36451  btwnconn1lem3  36452  btwnconn1lem4  36453  btwnconn1lem5  36454  btwnconn1lem6  36455  btwnconn1lem7  36456  btwnconn1lem8  36457  btwnconn1lem9  36458  btwnconn1lem10  36459  btwnconn1lem11  36460  btwnconn1lem12  36461  seglecgr12im  36473  seglecgr12  36474  ivthALT  36708  eqlkr  39735  lkrshp  39741  lshpkrlem5  39750  cvrval3  40049  4noncolr3  40089  4noncolr2  40090  4noncolr1  40091  athgt  40092  3dimlem2  40095  3dimlem3a  40096  3dimlem4a  40099  3dimlem4  40100  3dimlem4OLDN  40101  3dim2  40104  1cvratex  40109  hlatexch4  40117  ps-2b  40118  3atlem1  40119  3atlem2  40120  3atlem4  40122  3atlem5  40123  3atlem6  40124  llnnleat  40149  2atm  40163  ps-2c  40164  llnmlplnN  40175  lplnnlelln  40179  2atmat  40197  2llnjN  40203  lvoli2  40217  lvolnlelln  40220  4atlem3b  40234  4atlem9  40239  4atlem10a  40240  4atlem10  40242  4atlem11a  40243  4atlem11b  40244  4atlem12a  40246  4atlem12b  40247  4at  40249  4at2  40250  lplncvrlvol2  40251  2lplnj  40256  dalemswapyz  40292  dath2  40373  lneq2at  40414  2lnat  40420  cdlema1N  40427  cdlemb  40430  paddasslem15  40470  pmodlem1  40482  llnmod2i2  40499  llnexchb2lem  40504  llnexchb2  40505  dalawlem1  40507  dalawlem3  40509  dalawlem4  40510  dalawlem5  40511  dalawlem6  40512  dalawlem7  40513  dalawlem8  40514  dalawlem9  40515  dalawlem10  40516  dalawlem11  40517  dalawlem12  40518  dalawlem13  40519  dalawlem15  40521  dalaw  40522  osumcllem5N  40596  osumcllem6N  40597  osumcllem7N  40598  osumcllem9N  40600  osumcllem10N  40601  osumcllem11N  40602  pl42lem1N  40615  lhpexle3lem  40647  lhpmcvr5N  40663  lhp2atne  40670  lhp2at0ne  40672  4atexlemswapqr  40699  4atexlemex6  40710  ldilco  40752  ltrneq  40785  trlval2  40799  trlnidat  40809  cdlemd2  40835  cdlemd7  40840  cdlemd8  40841  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme11c  40897  cdleme11e  40899  cdleme11l  40905  cdleme11  40906  cdleme14  40909  cdleme15a  40910  cdleme15c  40912  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme16e  40918  cdleme16f  40919  cdleme0nex  40926  cdleme18d  40931  cdleme19b  40940  cdleme19d  40942  cdleme19e  40943  cdleme20f  40950  cdleme20i  40953  cdleme20k  40955  cdleme20l1  40956  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme21a  40961  cdleme21b  40962  cdleme21ct  40965  cdleme21d  40966  cdleme21e  40967  cdleme21f  40968  cdleme21h  40970  cdleme22eALTN  40981  cdleme22f2  40983  cdleme22g  40984  cdleme26e  40995  cdleme26eALTN  40997  cdleme26fALTN  40998  cdleme26f  40999  cdleme26f2ALTN  41000  cdleme26f2  41001  cdleme28a  41006  cdleme28b  41007  cdleme28  41009  cdleme29ex  41010  cdleme29c  41012  cdlemefrs29cpre1  41034  cdlemefr29exN  41038  cdlemefr32sn2aw  41040  cdlemefr29bpre0N  41042  cdlemefr29clN  41043  cdlemefr32fvaN  41045  cdlemefr32fva1  41046  cdlemefs32sn1aw  41050  cdleme43fsv1snlem  41056  cdleme41sn3a  41069  cdleme32fva  41073  cdleme32b  41078  cdleme32d  41080  cdleme32e  41081  cdleme32f  41082  cdleme32le  41083  cdleme35a  41084  cdleme35fnpq  41085  cdleme35b  41086  cdleme35c  41087  cdleme35d  41088  cdleme35e  41089  cdleme35f  41090  cdleme36a  41096  cdleme36m  41097  cdleme37m  41098  cdleme39a  41101  cdleme39n  41102  cdleme40m  41103  cdleme40n  41104  cdleme42e  41115  cdleme42f  41116  cdleme42g  41117  cdleme43bN  41126  cdleme43cN  41127  cdleme43dN  41128  cdleme46f2g2  41129  cdleme46f2g1  41130  cdleme17d2  41131  cdleme48b  41139  cdleme4gfv  41143  cdlemeg49le  41147  cdlemeg46c  41149  cdlemeg46fvaw  41152  cdlemeg46nlpq  41153  cdlemeg46frv  41161  cdlemeg46rgv  41164  cdlemeg46req  41165  cdlemeg46gfre  41168  cdleme50trn1  41185  cdleme50trn2a  41186  cdleme50trn2  41187  cdleme  41196  cdlemf  41199  trlord  41205  cdlemg2ce  41228  cdlemg7fvbwN  41243  cdlemg7aN  41261  cdlemg10bALTN  41272  cdlemg10a  41276  cdlemg10  41277  cdlemg12d  41282  cdlemg12f  41284  cdlemg12g  41285  cdlemg12  41286  cdlemg13a  41287  cdlemg13  41288  cdlemg17b  41298  cdlemg17dN  41299  cdlemg17dALTN  41300  cdlemg17e  41301  cdlemg17f  41302  cdlemg17g  41303  cdlemg17h  41304  cdlemg17i  41305  cdlemg17pq  41308  cdlemg17bq  41309  cdlemg17iqN  41310  cdlemg17  41313  cdlemg18d  41317  cdlemg18  41318  cdlemg19a  41319  cdlemg19  41320  cdlemg21  41322  cdlemg27a  41328  cdlemg28a  41329  cdlemg31b0N  41330  cdlemg27b  41332  cdlemg33b0  41337  cdlemg28b  41339  cdlemg28  41340  cdlemg33a  41342  cdlemg33  41347  cdlemg34  41348  cdlemg35  41349  cdlemg36  41350  ltrnco  41355  trlcone  41364  cdlemg44  41369  cdlemg47  41372  cdlemg48  41373  tendococl  41408  tendoplcl  41417  cdlemh1  41451  cdlemi  41456  cdlemj1  41457  cdlemj2  41458  tendocan  41460  cdlemk6  41473  cdlemki  41477  cdlemksat  41482  cdlemksv2  41483  cdlemk7  41484  cdlemk11  41485  cdlemk12  41486  cdlemkoatnle  41487  cdlemkole  41489  cdlemk14  41490  cdlemk15  41491  cdlemk16a  41492  cdlemk16  41493  cdlemk17  41494  cdlemk1u  41495  cdlemk5u  41497  cdlemk6u  41498  cdlemkuat  41502  cdlemk18  41504  cdlemk19  41505  cdlemk12u  41508  cdlemk21N  41509  cdlemk20  41510  cdlemkoatnle-2N  41511  cdlemk13-2N  41512  cdlemkole-2N  41513  cdlemk14-2N  41514  cdlemk15-2N  41515  cdlemk16-2N  41516  cdlemk17-2N  41517  cdlemk18-2N  41522  cdlemk19-2N  41523  cdlemk7u-2N  41524  cdlemk11u-2N  41525  cdlemk12u-2N  41526  cdlemk21-2N  41527  cdlemk20-2N  41528  cdlemk22  41529  cdlemk23-3  41538  cdlemk25-3  41540  cdlemk26b-3  41541  cdlemk27-3  41543  cdlemk28-3  41544  cdlemk33N  41545  cdlemk37  41550  cdlemky  41562  cdlemk11ta  41565  cdlemkid3N  41569  cdlemk11tc  41581  cdlemk11t  41582  cdlemk45  41583  cdlemk46  41584  cdlemk47  41585  cdlemk48  41586  cdlemk49  41587  cdlemk50  41588  cdlemk51  41589  cdlemk52  41590  cdlemk55b  41596  cdlemkyyN  41598  cdlemk55u1  41601  cdlemk55u  41602  cdlemk39u1  41603  cdlemk39u  41604  cdlemk56  41607  cdleml3N  41614  cdleml4N  41615  cdlemm10N  41754  dihord1  41854  dihord2a  41855  dihord2b  41856  dihord10  41859  dihord11c  41860  dihord2pre  41861  dihord4  41894  dihord5apre  41898  dihmeetlem1N  41926  dihglbcpreN  41936  dihjatc1  41947  dihjatc3  41949  dihmeetlem13N  41955  dihmeetlem20N  41962  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  hdmap14lem11  42514  hdmap14lem12  42515  flt4lem5  43244  monotuz  43530  congmul  43556  congsub  43559  rpnnen3lem  43620  ntrclsiso  44655  ntrclskb  44657  ntrclsk3  44658  wessf1ornlem  45761  infleinf  45945  lincdifsn  49055  itsclc0yqe  49392  itsclc0xyqsolr  49400  iscnrm3rlem8  49576  iscnrm3llem2  49579