Theorem simp11 1204

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp111  1303  simp211  1312  simp311  1321  omeulem1  8503  omeu  8506  ackbij1lem16  10132  coprimeprodsq  16722  pythagtriplem14  16742  pythagtrip  16748  mrelatglb  18468  subglsm  19587  lsmpropd  19591  mdetmul  22539  decpmatid  22686  isfil2  23772  filuni  23801  cxple2a  26636  isosctr  26759  nolesgn2o  27611  nolesgn2ores  27612  nogesgn1o  27613  nogesgn1ores  27614  nolt02o  27635  nogt01o  27636  sslttr  27749  cofcut2  27867  brbtwn2  28885  colinearalg  28890  ax5seglem3  28911  clwwlknonex2  30091  measres  34256  bayesth  34473  ofscom  36072  btwndiff  36092  ifscgr  36109  brofs2  36142  brifs2  36143  fscgr  36145  btwnconn1lem1  36152  btwnconn1lem2  36153  btwnconn1lem3  36154  btwnconn1lem4  36155  btwnconn1lem5  36156  btwnconn1lem6  36157  btwnconn1lem7  36158  btwnconn1lem8  36159  btwnconn1lem9  36160  btwnconn1lem10  36161  btwnconn1lem11  36162  btwnconn1lem12  36163  seglecgr12im  36175  seglecgr12  36176  ivthALT  36400  eqlkr  39219  lkrshp  39225  lshpkrlem5  39234  cvrval3  39533  4noncolr3  39573  4noncolr2  39574  4noncolr1  39575  athgt  39576  3dimlem2  39579  3dimlem3a  39580  3dimlem4a  39583  3dimlem4  39584  3dimlem4OLDN  39585  3dim2  39588  1cvratex  39593  hlatexch4  39601  ps-2b  39602  3atlem1  39603  3atlem2  39604  3atlem4  39606  3atlem5  39607  3atlem6  39608  llnnleat  39633  2atm  39647  ps-2c  39648  llnmlplnN  39659  lplnnlelln  39663  2atmat  39681  2llnjN  39687  lvoli2  39701  lvolnlelln  39704  4atlem3b  39718  4atlem9  39723  4atlem10a  39724  4atlem10  39726  4atlem11a  39727  4atlem11b  39728  4atlem12a  39730  4atlem12b  39731  4at  39733  4at2  39734  lplncvrlvol2  39735  2lplnj  39740  dalemswapyz  39776  dath2  39857  lneq2at  39898  2lnat  39904  cdlema1N  39911  cdlemb  39914  paddasslem15  39954  pmodlem1  39966  llnmod2i2  39983  llnexchb2lem  39988  llnexchb2  39989  dalawlem1  39991  dalawlem3  39993  dalawlem4  39994  dalawlem5  39995  dalawlem6  39996  dalawlem7  39997  dalawlem8  39998  dalawlem9  39999  dalawlem10  40000  dalawlem11  40001  dalawlem12  40002  dalawlem13  40003  dalawlem15  40005  dalaw  40006  osumcllem5N  40080  osumcllem6N  40081  osumcllem7N  40082  osumcllem9N  40084  osumcllem10N  40085  osumcllem11N  40086  pl42lem1N  40099  lhpexle3lem  40131  lhpmcvr5N  40147  lhp2atne  40154  lhp2at0ne  40156  4atexlemswapqr  40183  4atexlemex6  40194  ldilco  40236  ltrneq  40269  trlval2  40283  trlnidat  40293  cdlemd2  40319  cdlemd7  40324  cdlemd8  40325  cdleme7aa  40362  cdleme7c  40365  cdleme7d  40366  cdleme7e  40367  cdleme7ga  40368  cdleme7  40369  cdleme11c  40381  cdleme11e  40383  cdleme11l  40389  cdleme11  40390  cdleme14  40393  cdleme15a  40394  cdleme15c  40396  cdleme16b  40399  cdleme16c  40400  cdleme16d  40401  cdleme16e  40402  cdleme16f  40403  cdleme0nex  40410  cdleme18d  40415  cdleme19b  40424  cdleme19d  40426  cdleme19e  40427  cdleme20f  40434  cdleme20i  40437  cdleme20k  40439  cdleme20l1  40440  cdleme20l2  40441  cdleme20l  40442  cdleme20m  40443  cdleme21a  40445  cdleme21b  40446  cdleme21ct  40449  cdleme21d  40450  cdleme21e  40451  cdleme21f  40452  cdleme21h  40454  cdleme22eALTN  40465  cdleme22f2  40467  cdleme22g  40468  cdleme26e  40479  cdleme26eALTN  40481  cdleme26fALTN  40482  cdleme26f  40483  cdleme26f2ALTN  40484  cdleme26f2  40485  cdleme28a  40490  cdleme28b  40491  cdleme28  40493  cdleme29ex  40494  cdleme29c  40496  cdlemefrs29cpre1  40518  cdlemefr29exN  40522  cdlemefr32sn2aw  40524  cdlemefr29bpre0N  40526  cdlemefr29clN  40527  cdlemefr32fvaN  40529  cdlemefr32fva1  40530  cdlemefs32sn1aw  40534  cdleme43fsv1snlem  40540  cdleme41sn3a  40553  cdleme32fva  40557  cdleme32b  40562  cdleme32d  40564  cdleme32e  40565  cdleme32f  40566  cdleme32le  40567  cdleme35a  40568  cdleme35fnpq  40569  cdleme35b  40570  cdleme35c  40571  cdleme35d  40572  cdleme35e  40573  cdleme35f  40574  cdleme36a  40580  cdleme36m  40581  cdleme37m  40582  cdleme39a  40585  cdleme39n  40586  cdleme40m  40587  cdleme40n  40588  cdleme42e  40599  cdleme42f  40600  cdleme42g  40601  cdleme43bN  40610  cdleme43cN  40611  cdleme43dN  40612  cdleme46f2g2  40613  cdleme46f2g1  40614  cdleme17d2  40615  cdleme48b  40623  cdleme4gfv  40627  cdlemeg49le  40631  cdlemeg46c  40633  cdlemeg46fvaw  40636  cdlemeg46nlpq  40637  cdlemeg46frv  40645  cdlemeg46rgv  40648  cdlemeg46req  40649  cdlemeg46gfre  40652  cdleme50trn1  40669  cdleme50trn2a  40670  cdleme50trn2  40671  cdleme  40680  cdlemf  40683  trlord  40689  cdlemg2ce  40712  cdlemg7fvbwN  40727  cdlemg7aN  40745  cdlemg10bALTN  40756  cdlemg10a  40760  cdlemg10  40761  cdlemg12d  40766  cdlemg12f  40768  cdlemg12g  40769  cdlemg12  40770  cdlemg13a  40771  cdlemg13  40772  cdlemg17b  40782  cdlemg17dN  40783  cdlemg17dALTN  40784  cdlemg17e  40785  cdlemg17f  40786  cdlemg17g  40787  cdlemg17h  40788  cdlemg17i  40789  cdlemg17pq  40792  cdlemg17bq  40793  cdlemg17iqN  40794  cdlemg17  40797  cdlemg18d  40801  cdlemg18  40802  cdlemg19a  40803  cdlemg19  40804  cdlemg21  40806  cdlemg27a  40812  cdlemg28a  40813  cdlemg31b0N  40814  cdlemg27b  40816  cdlemg33b0  40821  cdlemg28b  40823  cdlemg28  40824  cdlemg33a  40826  cdlemg33  40831  cdlemg34  40832  cdlemg35  40833  cdlemg36  40834  ltrnco  40839  trlcone  40848  cdlemg44  40853  cdlemg47  40856  cdlemg48  40857  tendococl  40892  tendoplcl  40901  cdlemh1  40935  cdlemi  40940  cdlemj1  40941  cdlemj2  40942  tendocan  40944  cdlemk6  40957  cdlemki  40961  cdlemksat  40966  cdlemksv2  40967  cdlemk7  40968  cdlemk11  40969  cdlemk12  40970  cdlemkoatnle  40971  cdlemkole  40973  cdlemk14  40974  cdlemk15  40975  cdlemk16a  40976  cdlemk16  40977  cdlemk17  40978  cdlemk1u  40979  cdlemk5u  40981  cdlemk6u  40982  cdlemkuat  40986  cdlemk18  40988  cdlemk19  40989  cdlemk12u  40992  cdlemk21N  40993  cdlemk20  40994  cdlemkoatnle-2N  40995  cdlemk13-2N  40996  cdlemkole-2N  40997  cdlemk14-2N  40998  cdlemk15-2N  40999  cdlemk16-2N  41000  cdlemk17-2N  41001  cdlemk18-2N  41006  cdlemk19-2N  41007  cdlemk7u-2N  41008  cdlemk11u-2N  41009  cdlemk12u-2N  41010  cdlemk21-2N  41011  cdlemk20-2N  41012  cdlemk22  41013  cdlemk23-3  41022  cdlemk25-3  41024  cdlemk26b-3  41025  cdlemk27-3  41027  cdlemk28-3  41028  cdlemk33N  41029  cdlemk37  41034  cdlemky  41046  cdlemk11ta  41049  cdlemkid3N  41053  cdlemk11tc  41065  cdlemk11t  41066  cdlemk45  41067  cdlemk46  41068  cdlemk47  41069  cdlemk48  41070  cdlemk49  41071  cdlemk50  41072  cdlemk51  41073  cdlemk52  41074  cdlemk55b  41080  cdlemkyyN  41082  cdlemk55u1  41085  cdlemk55u  41086  cdlemk39u1  41087  cdlemk39u  41088  cdlemk56  41091  cdleml3N  41098  cdleml4N  41099  cdlemm10N  41238  dihord1  41338  dihord2a  41339  dihord2b  41340  dihord10  41343  dihord11c  41344  dihord2pre  41345  dihord4  41378  dihord5apre  41382  dihmeetlem1N  41410  dihglbcpreN  41420  dihjatc1  41431  dihjatc3  41433  dihmeetlem13N  41439  dihmeetlem20N  41446  baerlem3lem2  41830  baerlem5alem2  41831  baerlem5blem2  41832  hdmap14lem11  41998  hdmap14lem12  41999  flt4lem5  42769  monotuz  43059  congmul  43085  congsub  43088  rpnnen3lem  43149  ntrclsiso  44185  ntrclskb  44187  ntrclsk3  44188  wessf1ornlem  45307  infleinf  45495  lincdifsn  48550  itsclc0yqe  48887  itsclc0xyqsolr  48895  iscnrm3rlem8  49072  iscnrm3llem2  49075