Theorem simp11 1205

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  simp111  1304  simp211  1313  simp311  1322  omeulem1  8288  omeu  8291  ackbij1lem16  9814  coprimeprodsq  16324  pythagtriplem14  16344  pythagtrip  16350  mrelatglb  18020  subglsm  19017  lsmpropd  19021  mdetmul  21474  decpmatid  21621  isfil2  22707  filuni  22736  cxple2a  25541  isosctr  25658  brbtwn2  26950  colinearalg  26955  ax5seglem3  26976  clwwlknonex2  28146  measres  31856  bayesth  32072  nolesgn2o  33560  nolesgn2ores  33561  nogesgn1o  33562  nogesgn1ores  33563  nolt02o  33584  nogt01o  33585  sslttr  33687  cofcut2  33777  ofscom  33995  btwndiff  34015  ifscgr  34032  brofs2  34065  brifs2  34066  fscgr  34068  btwnconn1lem1  34075  btwnconn1lem2  34076  btwnconn1lem3  34077  btwnconn1lem4  34078  btwnconn1lem5  34079  btwnconn1lem6  34080  btwnconn1lem7  34081  btwnconn1lem8  34082  btwnconn1lem9  34083  btwnconn1lem10  34084  btwnconn1lem11  34085  btwnconn1lem12  34086  seglecgr12im  34098  seglecgr12  34099  ivthALT  34210  eqlkr  36799  lkrshp  36805  lshpkrlem5  36814  cvrval3  37113  4noncolr3  37153  4noncolr2  37154  4noncolr1  37155  athgt  37156  3dimlem2  37159  3dimlem3a  37160  3dimlem4a  37163  3dimlem4  37164  3dimlem4OLDN  37165  3dim2  37168  1cvratex  37173  hlatexch4  37181  ps-2b  37182  3atlem1  37183  3atlem2  37184  3atlem4  37186  3atlem5  37187  3atlem6  37188  llnnleat  37213  2atm  37227  ps-2c  37228  llnmlplnN  37239  lplnnlelln  37243  2atmat  37261  2llnjN  37267  lvoli2  37281  lvolnlelln  37284  4atlem3b  37298  4atlem9  37303  4atlem10a  37304  4atlem10  37306  4atlem11a  37307  4atlem11b  37308  4atlem12a  37310  4atlem12b  37311  4at  37313  4at2  37314  lplncvrlvol2  37315  2lplnj  37320  dalemswapyz  37356  dath2  37437  lneq2at  37478  2lnat  37484  cdlema1N  37491  cdlemb  37494  paddasslem15  37534  pmodlem1  37546  llnmod2i2  37563  llnexchb2lem  37568  llnexchb2  37569  dalawlem1  37571  dalawlem3  37573  dalawlem4  37574  dalawlem5  37575  dalawlem6  37576  dalawlem7  37577  dalawlem8  37578  dalawlem9  37579  dalawlem10  37580  dalawlem11  37581  dalawlem12  37582  dalawlem13  37583  dalawlem15  37585  dalaw  37586  osumcllem5N  37660  osumcllem6N  37661  osumcllem7N  37662  osumcllem9N  37664  osumcllem10N  37665  osumcllem11N  37666  pl42lem1N  37679  lhpexle3lem  37711  lhpmcvr5N  37727  lhp2atne  37734  lhp2at0ne  37736  4atexlemswapqr  37763  4atexlemex6  37774  ldilco  37816  ltrneq  37849  trlval2  37863  trlnidat  37873  cdlemd2  37899  cdlemd7  37904  cdlemd8  37905  cdleme7aa  37942  cdleme7c  37945  cdleme7d  37946  cdleme7e  37947  cdleme7ga  37948  cdleme7  37949  cdleme11c  37961  cdleme11e  37963  cdleme11l  37969  cdleme11  37970  cdleme14  37973  cdleme15a  37974  cdleme15c  37976  cdleme16b  37979  cdleme16c  37980  cdleme16d  37981  cdleme16e  37982  cdleme16f  37983  cdleme0nex  37990  cdleme18d  37995  cdleme19b  38004  cdleme19d  38006  cdleme19e  38007  cdleme20f  38014  cdleme20i  38017  cdleme20k  38019  cdleme20l1  38020  cdleme20l2  38021  cdleme20l  38022  cdleme20m  38023  cdleme21a  38025  cdleme21b  38026  cdleme21ct  38029  cdleme21d  38030  cdleme21e  38031  cdleme21f  38032  cdleme21h  38034  cdleme22eALTN  38045  cdleme22f2  38047  cdleme22g  38048  cdleme26e  38059  cdleme26eALTN  38061  cdleme26fALTN  38062  cdleme26f  38063  cdleme26f2ALTN  38064  cdleme26f2  38065  cdleme28a  38070  cdleme28b  38071  cdleme28  38073  cdleme29ex  38074  cdleme29c  38076  cdlemefrs29cpre1  38098  cdlemefr29exN  38102  cdlemefr32sn2aw  38104  cdlemefr29bpre0N  38106  cdlemefr29clN  38107  cdlemefr32fvaN  38109  cdlemefr32fva1  38110  cdlemefs32sn1aw  38114  cdleme43fsv1snlem  38120  cdleme41sn3a  38133  cdleme32fva  38137  cdleme32b  38142  cdleme32d  38144  cdleme32e  38145  cdleme32f  38146  cdleme32le  38147  cdleme35a  38148  cdleme35fnpq  38149  cdleme35b  38150  cdleme35c  38151  cdleme35d  38152  cdleme35e  38153  cdleme35f  38154  cdleme36a  38160  cdleme36m  38161  cdleme37m  38162  cdleme39a  38165  cdleme39n  38166  cdleme40m  38167  cdleme40n  38168  cdleme42e  38179  cdleme42f  38180  cdleme42g  38181  cdleme43bN  38190  cdleme43cN  38191  cdleme43dN  38192  cdleme46f2g2  38193  cdleme46f2g1  38194  cdleme17d2  38195  cdleme48b  38203  cdleme4gfv  38207  cdlemeg49le  38211  cdlemeg46c  38213  cdlemeg46fvaw  38216  cdlemeg46nlpq  38217  cdlemeg46frv  38225  cdlemeg46rgv  38228  cdlemeg46req  38229  cdlemeg46gfre  38232  cdleme50trn1  38249  cdleme50trn2a  38250  cdleme50trn2  38251  cdleme  38260  cdlemf  38263  trlord  38269  cdlemg2ce  38292  cdlemg7fvbwN  38307  cdlemg7aN  38325  cdlemg10bALTN  38336  cdlemg10a  38340  cdlemg10  38341  cdlemg12d  38346  cdlemg12f  38348  cdlemg12g  38349  cdlemg12  38350  cdlemg13a  38351  cdlemg13  38352  cdlemg17b  38362  cdlemg17dN  38363  cdlemg17dALTN  38364  cdlemg17e  38365  cdlemg17f  38366  cdlemg17g  38367  cdlemg17h  38368  cdlemg17i  38369  cdlemg17pq  38372  cdlemg17bq  38373  cdlemg17iqN  38374  cdlemg17  38377  cdlemg18d  38381  cdlemg18  38382  cdlemg19a  38383  cdlemg19  38384  cdlemg21  38386  cdlemg27a  38392  cdlemg28a  38393  cdlemg31b0N  38394  cdlemg27b  38396  cdlemg33b0  38401  cdlemg28b  38403  cdlemg28  38404  cdlemg33a  38406  cdlemg33  38411  cdlemg34  38412  cdlemg35  38413  cdlemg36  38414  ltrnco  38419  trlcone  38428  cdlemg44  38433  cdlemg47  38436  cdlemg48  38437  tendococl  38472  tendoplcl  38481  cdlemh1  38515  cdlemi  38520  cdlemj1  38521  cdlemj2  38522  tendocan  38524  cdlemk6  38537  cdlemki  38541  cdlemksat  38546  cdlemksv2  38547  cdlemk7  38548  cdlemk11  38549  cdlemk12  38550  cdlemkoatnle  38551  cdlemkole  38553  cdlemk14  38554  cdlemk15  38555  cdlemk16a  38556  cdlemk16  38557  cdlemk17  38558  cdlemk1u  38559  cdlemk5u  38561  cdlemk6u  38562  cdlemkuat  38566  cdlemk18  38568  cdlemk19  38569  cdlemk12u  38572  cdlemk21N  38573  cdlemk20  38574  cdlemkoatnle-2N  38575  cdlemk13-2N  38576  cdlemkole-2N  38577  cdlemk14-2N  38578  cdlemk15-2N  38579  cdlemk16-2N  38580  cdlemk17-2N  38581  cdlemk18-2N  38586  cdlemk19-2N  38587  cdlemk7u-2N  38588  cdlemk11u-2N  38589  cdlemk12u-2N  38590  cdlemk21-2N  38591  cdlemk20-2N  38592  cdlemk22  38593  cdlemk23-3  38602  cdlemk25-3  38604  cdlemk26b-3  38605  cdlemk27-3  38607  cdlemk28-3  38608  cdlemk33N  38609  cdlemk37  38614  cdlemky  38626  cdlemk11ta  38629  cdlemkid3N  38633  cdlemk11tc  38645  cdlemk11t  38646  cdlemk45  38647  cdlemk46  38648  cdlemk47  38649  cdlemk48  38650  cdlemk49  38651  cdlemk50  38652  cdlemk51  38653  cdlemk52  38654  cdlemk55b  38660  cdlemkyyN  38662  cdlemk55u1  38665  cdlemk55u  38666  cdlemk39u1  38667  cdlemk39u  38668  cdlemk56  38671  cdleml3N  38678  cdleml4N  38679  cdlemm10N  38818  dihord1  38918  dihord2a  38919  dihord2b  38920  dihord10  38923  dihord11c  38924  dihord2pre  38925  dihord4  38958  dihord5apre  38962  dihmeetlem1N  38990  dihglbcpreN  39000  dihjatc1  39011  dihjatc3  39013  dihmeetlem13N  39019  dihmeetlem20N  39026  baerlem3lem2  39410  baerlem5alem2  39411  baerlem5blem2  39412  hdmap14lem11  39578  hdmap14lem12  39579  flt4lem5  40131  monotuz  40407  congmul  40433  congsub  40436  rpnnen3lem  40497  ntrclsiso  41295  ntrclskb  41297  ntrclsk3  41298  wessf1ornlem  42336  infleinf  42525  lincdifsn  45381  itsclc0yqe  45723  itsclc0xyqsolr  45731  iscnrm3rlem8  45857  iscnrm3llem2  45860