Theorem simp11 1199

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp111  1298  simp211  1307  simp311  1316  omeulem1  8207  omeu  8210  ackbij1lem16  9656  coprimeprodsq  16144  pythagtriplem14  16164  pythagtrip  16170  mrelatglb  17793  subglsm  18798  lsmpropd  18802  mdetmul  21231  decpmatid  21377  isfil2  22463  filuni  22492  cxple2a  25281  isosctr  25398  brbtwn2  26690  colinearalg  26695  ax5seglem3  26716  clwwlknonex2  27887  measres  31481  bayesth  31697  nolesgn2o  33178  nolesgn2ores  33179  nolt02o  33199  ofscom  33468  btwndiff  33488  ifscgr  33505  brofs2  33538  brifs2  33539  fscgr  33541  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem7  33554  btwnconn1lem8  33555  btwnconn1lem9  33556  btwnconn1lem10  33557  btwnconn1lem11  33558  btwnconn1lem12  33559  seglecgr12im  33571  seglecgr12  33572  ivthALT  33683  eqlkr  36234  lkrshp  36240  lshpkrlem5  36249  cvrval3  36548  4noncolr3  36588  4noncolr2  36589  4noncolr1  36590  athgt  36591  3dimlem2  36594  3dimlem3a  36595  3dimlem4a  36598  3dimlem4  36599  3dimlem4OLDN  36600  3dim2  36603  1cvratex  36608  hlatexch4  36616  ps-2b  36617  3atlem1  36618  3atlem2  36619  3atlem4  36621  3atlem5  36622  3atlem6  36623  llnnleat  36648  2atm  36662  ps-2c  36663  llnmlplnN  36674  lplnnlelln  36678  2atmat  36696  2llnjN  36702  lvoli2  36716  lvolnlelln  36719  4atlem3b  36733  4atlem9  36738  4atlem10a  36739  4atlem10  36741  4atlem11a  36742  4atlem11b  36743  4atlem12a  36745  4atlem12b  36746  4at  36748  4at2  36749  lplncvrlvol2  36750  2lplnj  36755  dalemswapyz  36791  dath2  36872  lneq2at  36913  2lnat  36919  cdlema1N  36926  cdlemb  36929  paddasslem15  36969  pmodlem1  36981  llnmod2i2  36998  llnexchb2lem  37003  llnexchb2  37004  dalawlem1  37006  dalawlem3  37008  dalawlem4  37009  dalawlem5  37010  dalawlem6  37011  dalawlem7  37012  dalawlem8  37013  dalawlem9  37014  dalawlem10  37015  dalawlem11  37016  dalawlem12  37017  dalawlem13  37018  dalawlem15  37020  dalaw  37021  osumcllem5N  37095  osumcllem6N  37096  osumcllem7N  37097  osumcllem9N  37099  osumcllem10N  37100  osumcllem11N  37101  pl42lem1N  37114  lhpexle3lem  37146  lhpmcvr5N  37162  lhp2atne  37169  lhp2at0ne  37171  4atexlemswapqr  37198  4atexlemex6  37209  ldilco  37251  ltrneq  37284  trlval2  37298  trlnidat  37308  cdlemd2  37334  cdlemd7  37339  cdlemd8  37340  cdleme7aa  37377  cdleme7c  37380  cdleme7d  37381  cdleme7e  37382  cdleme7ga  37383  cdleme7  37384  cdleme11c  37396  cdleme11e  37398  cdleme11l  37404  cdleme11  37405  cdleme14  37408  cdleme15a  37409  cdleme15c  37411  cdleme16b  37414  cdleme16c  37415  cdleme16d  37416  cdleme16e  37417  cdleme16f  37418  cdleme0nex  37425  cdleme18d  37430  cdleme19b  37439  cdleme19d  37441  cdleme19e  37442  cdleme20f  37449  cdleme20i  37452  cdleme20k  37454  cdleme20l1  37455  cdleme20l2  37456  cdleme20l  37457  cdleme20m  37458  cdleme21a  37460  cdleme21b  37461  cdleme21ct  37464  cdleme21d  37465  cdleme21e  37466  cdleme21f  37467  cdleme21h  37469  cdleme22eALTN  37480  cdleme22f2  37482  cdleme22g  37483  cdleme26e  37494  cdleme26eALTN  37496  cdleme26fALTN  37497  cdleme26f  37498  cdleme26f2ALTN  37499  cdleme26f2  37500  cdleme28a  37505  cdleme28b  37506  cdleme28  37508  cdleme29ex  37509  cdleme29c  37511  cdlemefrs29cpre1  37533  cdlemefr29exN  37537  cdlemefr32sn2aw  37539  cdlemefr29bpre0N  37541  cdlemefr29clN  37542  cdlemefr32fvaN  37544  cdlemefr32fva1  37545  cdlemefs32sn1aw  37549  cdleme43fsv1snlem  37555  cdleme41sn3a  37568  cdleme32fva  37572  cdleme32b  37577  cdleme32d  37579  cdleme32e  37580  cdleme32f  37581  cdleme32le  37582  cdleme35a  37583  cdleme35fnpq  37584  cdleme35b  37585  cdleme35c  37586  cdleme35d  37587  cdleme35e  37588  cdleme35f  37589  cdleme36a  37595  cdleme36m  37596  cdleme37m  37597  cdleme39a  37600  cdleme39n  37601  cdleme40m  37602  cdleme40n  37603  cdleme42e  37614  cdleme42f  37615  cdleme42g  37616  cdleme43bN  37625  cdleme43cN  37626  cdleme43dN  37627  cdleme46f2g2  37628  cdleme46f2g1  37629  cdleme17d2  37630  cdleme48b  37638  cdleme4gfv  37642  cdlemeg49le  37646  cdlemeg46c  37648  cdlemeg46fvaw  37651  cdlemeg46nlpq  37652  cdlemeg46frv  37660  cdlemeg46rgv  37663  cdlemeg46req  37664  cdlemeg46gfre  37667  cdleme50trn1  37684  cdleme50trn2a  37685  cdleme50trn2  37686  cdleme  37695  cdlemf  37698  trlord  37704  cdlemg2ce  37727  cdlemg7fvbwN  37742  cdlemg7aN  37760  cdlemg10bALTN  37771  cdlemg10a  37775  cdlemg10  37776  cdlemg12d  37781  cdlemg12f  37783  cdlemg12g  37784  cdlemg12  37785  cdlemg13a  37786  cdlemg13  37787  cdlemg17b  37797  cdlemg17dN  37798  cdlemg17dALTN  37799  cdlemg17e  37800  cdlemg17f  37801  cdlemg17g  37802  cdlemg17h  37803  cdlemg17i  37804  cdlemg17pq  37807  cdlemg17bq  37808  cdlemg17iqN  37809  cdlemg17  37812  cdlemg18d  37816  cdlemg18  37817  cdlemg19a  37818  cdlemg19  37819  cdlemg21  37821  cdlemg27a  37827  cdlemg28a  37828  cdlemg31b0N  37829  cdlemg27b  37831  cdlemg33b0  37836  cdlemg28b  37838  cdlemg28  37839  cdlemg33a  37841  cdlemg33  37846  cdlemg34  37847  cdlemg35  37848  cdlemg36  37849  ltrnco  37854  trlcone  37863  cdlemg44  37868  cdlemg47  37871  cdlemg48  37872  tendococl  37907  tendoplcl  37916  cdlemh1  37950  cdlemi  37955  cdlemj1  37956  cdlemj2  37957  tendocan  37959  cdlemk6  37972  cdlemki  37976  cdlemksat  37981  cdlemksv2  37982  cdlemk7  37983  cdlemk11  37984  cdlemk12  37985  cdlemkoatnle  37986  cdlemkole  37988  cdlemk14  37989  cdlemk15  37990  cdlemk16a  37991  cdlemk16  37992  cdlemk17  37993  cdlemk1u  37994  cdlemk5u  37996  cdlemk6u  37997  cdlemkuat  38001  cdlemk18  38003  cdlemk19  38004  cdlemk12u  38007  cdlemk21N  38008  cdlemk20  38009  cdlemkoatnle-2N  38010  cdlemk13-2N  38011  cdlemkole-2N  38012  cdlemk14-2N  38013  cdlemk15-2N  38014  cdlemk16-2N  38015  cdlemk17-2N  38016  cdlemk18-2N  38021  cdlemk19-2N  38022  cdlemk7u-2N  38023  cdlemk11u-2N  38024  cdlemk12u-2N  38025  cdlemk21-2N  38026  cdlemk20-2N  38027  cdlemk22  38028  cdlemk23-3  38037  cdlemk25-3  38039  cdlemk26b-3  38040  cdlemk27-3  38042  cdlemk28-3  38043  cdlemk33N  38044  cdlemk37  38049  cdlemky  38061  cdlemk11ta  38064  cdlemkid3N  38068  cdlemk11tc  38080  cdlemk11t  38081  cdlemk45  38082  cdlemk46  38083  cdlemk47  38084  cdlemk48  38085  cdlemk49  38086  cdlemk50  38087  cdlemk51  38088  cdlemk52  38089  cdlemk55b  38095  cdlemkyyN  38097  cdlemk55u1  38100  cdlemk55u  38101  cdlemk39u1  38102  cdlemk39u  38103  cdlemk56  38106  cdleml3N  38113  cdleml4N  38114  cdlemm10N  38253  dihord1  38353  dihord2a  38354  dihord2b  38355  dihord10  38358  dihord11c  38359  dihord2pre  38360  dihord4  38393  dihord5apre  38397  dihmeetlem1N  38425  dihglbcpreN  38435  dihjatc1  38446  dihjatc3  38448  dihmeetlem13N  38454  dihmeetlem20N  38461  baerlem3lem2  38845  baerlem5alem2  38846  baerlem5blem2  38847  hdmap14lem11  39013  hdmap14lem12  39014  monotuz  39536  congmul  39562  congsub  39565  rpnnen3lem  39626  ntrclsiso  40415  ntrclskb  40417  ntrclsk3  40418  wessf1ornlem  41443  infleinf  41638  lincdifsn  44478  itsclc0yqe  44747  itsclc0xyqsolr  44755