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  8593  omeu  8596  ackbij1lem16  10315  coprimeprodsq  16991  pythagtriplem14  17011  pythagtrip  17017  mrelatglb  18739  subglsm  19892  lsmpropd  19896  mdetmul  22943  decpmatid  23093  isfil2  24180  filuni  24209  cxple2a  27032  isosctr  27154  flt4lem5  27985  nolesgn2o  28033  nolesgn2ores  28034  nogesgn1o  28035  nogesgn1ores  28036  nolt02o  28057  nogt01o  28058  sltstr  28178  cofcut2  28313  brbtwn2  29488  colinearalg  29493  ax5seglem3  29514  clwwlknonex2  30705  measres  34901  bayesth  35117  ofscom  36864  btwndiff  36884  ifscgr  36901  brofs2  36934  brifs2  36935  fscgr  36937  btwnconn1lem1  36944  btwnconn1lem2  36945  btwnconn1lem3  36946  btwnconn1lem4  36947  btwnconn1lem5  36948  btwnconn1lem6  36949  btwnconn1lem7  36950  btwnconn1lem8  36951  btwnconn1lem9  36952  btwnconn1lem10  36953  btwnconn1lem11  36954  btwnconn1lem12  36955  seglecgr12im  36967  seglecgr12  36968  ivthALT  37215  eqlkr  40249  lkrshp  40255  lshpkrlem5  40264  cvrval3  40563  4noncolr3  40603  4noncolr2  40604  4noncolr1  40605  athgt  40606  3dimlem2  40609  3dimlem3a  40610  3dimlem4a  40613  3dimlem4  40614  3dimlem4OLDN  40615  3dim2  40618  1cvratex  40623  hlatexch4  40631  ps-2b  40632  3atlem1  40633  3atlem2  40634  3atlem4  40636  3atlem5  40637  3atlem6  40638  llnnleat  40663  2atm  40677  ps-2c  40678  llnmlplnN  40689  lplnnlelln  40693  2atmat  40711  2llnjN  40717  lvoli2  40731  lvolnlelln  40734  4atlem3b  40748  4atlem9  40753  4atlem10a  40754  4atlem10  40756  4atlem11a  40757  4atlem11b  40758  4atlem12a  40760  4atlem12b  40761  4at  40763  4at2  40764  lplncvrlvol2  40765  2lplnj  40770  dalemswapyz  40806  dath2  40887  lneq2at  40928  2lnat  40934  cdlema1N  40941  cdlemb  40944  paddasslem15  40984  pmodlem1  40996  llnmod2i2  41013  llnexchb2lem  41018  llnexchb2  41019  dalawlem1  41021  dalawlem3  41023  dalawlem4  41024  dalawlem5  41025  dalawlem6  41026  dalawlem7  41027  dalawlem8  41028  dalawlem9  41029  dalawlem10  41030  dalawlem11  41031  dalawlem12  41032  dalawlem13  41033  dalawlem15  41035  dalaw  41036  osumcllem5N  41110  osumcllem6N  41111  osumcllem7N  41112  osumcllem9N  41114  osumcllem10N  41115  osumcllem11N  41116  pl42lem1N  41129  lhpexle3lem  41161  lhpmcvr5N  41177  lhp2atne  41184  lhp2at0ne  41186  4atexlemswapqr  41213  4atexlemex6  41224  ldilco  41266  ltrneq  41299  trlval2  41313  trlnidat  41323  cdlemd2  41349  cdlemd7  41354  cdlemd8  41355  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme11c  41411  cdleme11e  41413  cdleme11l  41419  cdleme11  41420  cdleme14  41423  cdleme15a  41424  cdleme15c  41426  cdleme16b  41429  cdleme16c  41430  cdleme16d  41431  cdleme16e  41432  cdleme16f  41433  cdleme0nex  41440  cdleme18d  41445  cdleme19b  41454  cdleme19d  41456  cdleme19e  41457  cdleme20f  41464  cdleme20i  41467  cdleme20k  41469  cdleme20l1  41470  cdleme20l2  41471  cdleme20l  41472  cdleme20m  41473  cdleme21a  41475  cdleme21b  41476  cdleme21ct  41479  cdleme21d  41480  cdleme21e  41481  cdleme21f  41482  cdleme21h  41484  cdleme22eALTN  41495  cdleme22f2  41497  cdleme22g  41498  cdleme26e  41509  cdleme26eALTN  41511  cdleme26fALTN  41512  cdleme26f  41513  cdleme26f2ALTN  41514  cdleme26f2  41515  cdleme28a  41520  cdleme28b  41521  cdleme28  41523  cdleme29ex  41524  cdleme29c  41526  cdlemefrs29cpre1  41548  cdlemefr29exN  41552  cdlemefr32sn2aw  41554  cdlemefr29bpre0N  41556  cdlemefr29clN  41557  cdlemefr32fvaN  41559  cdlemefr32fva1  41560  cdlemefs32sn1aw  41564  cdleme43fsv1snlem  41570  cdleme41sn3a  41583  cdleme32fva  41587  cdleme32b  41592  cdleme32d  41594  cdleme32e  41595  cdleme32f  41596  cdleme32le  41597  cdleme35a  41598  cdleme35fnpq  41599  cdleme35b  41600  cdleme35c  41601  cdleme35d  41602  cdleme35e  41603  cdleme35f  41604  cdleme36a  41610  cdleme36m  41611  cdleme37m  41612  cdleme39a  41615  cdleme39n  41616  cdleme40m  41617  cdleme40n  41618  cdleme42e  41629  cdleme42f  41630  cdleme42g  41631  cdleme43bN  41640  cdleme43cN  41641  cdleme43dN  41642  cdleme46f2g2  41643  cdleme46f2g1  41644  cdleme17d2  41645  cdleme48b  41653  cdleme4gfv  41657  cdlemeg49le  41661  cdlemeg46c  41663  cdlemeg46fvaw  41666  cdlemeg46nlpq  41667  cdlemeg46frv  41675  cdlemeg46rgv  41678  cdlemeg46req  41679  cdlemeg46gfre  41682  cdleme50trn1  41699  cdleme50trn2a  41700  cdleme50trn2  41701  cdleme  41710  cdlemf  41713  trlord  41719  cdlemg2ce  41742  cdlemg7fvbwN  41757  cdlemg7aN  41775  cdlemg10bALTN  41786  cdlemg10a  41790  cdlemg10  41791  cdlemg12d  41796  cdlemg12f  41798  cdlemg12g  41799  cdlemg12  41800  cdlemg13a  41801  cdlemg13  41802  cdlemg17b  41812  cdlemg17dN  41813  cdlemg17dALTN  41814  cdlemg17e  41815  cdlemg17f  41816  cdlemg17g  41817  cdlemg17h  41818  cdlemg17i  41819  cdlemg17pq  41822  cdlemg17bq  41823  cdlemg17iqN  41824  cdlemg17  41827  cdlemg18d  41831  cdlemg18  41832  cdlemg19a  41833  cdlemg19  41834  cdlemg21  41836  cdlemg27a  41842  cdlemg28a  41843  cdlemg31b0N  41844  cdlemg27b  41846  cdlemg33b0  41851  cdlemg28b  41853  cdlemg28  41854  cdlemg33a  41856  cdlemg33  41861  cdlemg34  41862  cdlemg35  41863  cdlemg36  41864  ltrnco  41869  trlcone  41878  cdlemg44  41883  cdlemg47  41886  cdlemg48  41887  tendococl  41922  tendoplcl  41931  cdlemh1  41965  cdlemi  41970  cdlemj1  41971  cdlemj2  41972  tendocan  41974  cdlemk6  41987  cdlemki  41991  cdlemksat  41996  cdlemksv2  41997  cdlemk7  41998  cdlemk11  41999  cdlemk12  42000  cdlemkoatnle  42001  cdlemkole  42003  cdlemk14  42004  cdlemk15  42005  cdlemk16a  42006  cdlemk16  42007  cdlemk17  42008  cdlemk1u  42009  cdlemk5u  42011  cdlemk6u  42012  cdlemkuat  42016  cdlemk18  42018  cdlemk19  42019  cdlemk12u  42022  cdlemk21N  42023  cdlemk20  42024  cdlemkoatnle-2N  42025  cdlemk13-2N  42026  cdlemkole-2N  42027  cdlemk14-2N  42028  cdlemk15-2N  42029  cdlemk16-2N  42030  cdlemk17-2N  42031  cdlemk18-2N  42036  cdlemk19-2N  42037  cdlemk7u-2N  42038  cdlemk11u-2N  42039  cdlemk12u-2N  42040  cdlemk21-2N  42041  cdlemk20-2N  42042  cdlemk22  42043  cdlemk23-3  42052  cdlemk25-3  42054  cdlemk26b-3  42055  cdlemk27-3  42057  cdlemk28-3  42058  cdlemk33N  42059  cdlemk37  42064  cdlemky  42076  cdlemk11ta  42079  cdlemkid3N  42083  cdlemk11tc  42095  cdlemk11t  42096  cdlemk45  42097  cdlemk46  42098  cdlemk47  42099  cdlemk48  42100  cdlemk49  42101  cdlemk50  42102  cdlemk51  42103  cdlemk52  42104  cdlemk55b  42110  cdlemkyyN  42112  cdlemk55u1  42115  cdlemk55u  42116  cdlemk39u1  42117  cdlemk39u  42118  cdlemk56  42121  cdleml3N  42128  cdleml4N  42129  cdlemm10N  42268  dihord1  42368  dihord2a  42369  dihord2b  42370  dihord10  42373  dihord11c  42374  dihord2pre  42375  dihord4  42408  dihord5apre  42412  dihmeetlem1N  42440  dihglbcpreN  42450  dihjatc1  42461  dihjatc3  42463  dihmeetlem13N  42469  dihmeetlem20N  42476  baerlem3lem2  42860  baerlem5alem2  42861  baerlem5blem2  42862  hdmap14lem11  43028  hdmap14lem12  43029  monotuz  44041  congmul  44067  congsub  44070  rpnnen3lem  44131  ntrclsiso  45160  ntrclskb  45162  ntrclsk3  45163  dmstructnn  46019  wessf1ornlem  46293  infleinf  46476  lincdifsn  49629  itsclc0yqe  49966  itsclc0xyqsolr  49974  iscnrm3rlem8  50154  iscnrm3llem2  50157