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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp111  1304  simp211  1313  simp311  1322  omeulem1  8519  omeu  8522  ackbij1lem16  10156  coprimeprodsq  16748  pythagtriplem14  16768  pythagtrip  16774  mrelatglb  18495  subglsm  19614  lsmpropd  19618  mdetmul  22579  decpmatid  22726  isfil2  23812  filuni  23841  cxple2a  26676  isosctr  26799  nolesgn2o  27651  nolesgn2ores  27652  nogesgn1o  27653  nogesgn1ores  27654  nolt02o  27675  nogt01o  27676  sltstr  27795  cofcut2  27930  brbtwn2  28990  colinearalg  28995  ax5seglem3  29016  clwwlknonex2  30196  measres  34399  bayesth  34616  ofscom  36220  btwndiff  36240  ifscgr  36257  brofs2  36290  brifs2  36291  fscgr  36293  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem7  36306  btwnconn1lem8  36307  btwnconn1lem9  36308  btwnconn1lem10  36309  btwnconn1lem11  36310  btwnconn1lem12  36311  seglecgr12im  36323  seglecgr12  36324  ivthALT  36548  eqlkr  39469  lkrshp  39475  lshpkrlem5  39484  cvrval3  39783  4noncolr3  39823  4noncolr2  39824  4noncolr1  39825  athgt  39826  3dimlem2  39829  3dimlem3a  39830  3dimlem4a  39833  3dimlem4  39834  3dimlem4OLDN  39835  3dim2  39838  1cvratex  39843  hlatexch4  39851  ps-2b  39852  3atlem1  39853  3atlem2  39854  3atlem4  39856  3atlem5  39857  3atlem6  39858  llnnleat  39883  2atm  39897  ps-2c  39898  llnmlplnN  39909  lplnnlelln  39913  2atmat  39931  2llnjN  39937  lvoli2  39951  lvolnlelln  39954  4atlem3b  39968  4atlem9  39973  4atlem10a  39974  4atlem10  39976  4atlem11a  39977  4atlem11b  39978  4atlem12a  39980  4atlem12b  39981  4at  39983  4at2  39984  lplncvrlvol2  39985  2lplnj  39990  dalemswapyz  40026  dath2  40107  lneq2at  40148  2lnat  40154  cdlema1N  40161  cdlemb  40164  paddasslem15  40204  pmodlem1  40216  llnmod2i2  40233  llnexchb2lem  40238  llnexchb2  40239  dalawlem1  40241  dalawlem3  40243  dalawlem4  40244  dalawlem5  40245  dalawlem6  40246  dalawlem7  40247  dalawlem8  40248  dalawlem9  40249  dalawlem10  40250  dalawlem11  40251  dalawlem12  40252  dalawlem13  40253  dalawlem15  40255  dalaw  40256  osumcllem5N  40330  osumcllem6N  40331  osumcllem7N  40332  osumcllem9N  40334  osumcllem10N  40335  osumcllem11N  40336  pl42lem1N  40349  lhpexle3lem  40381  lhpmcvr5N  40397  lhp2atne  40404  lhp2at0ne  40406  4atexlemswapqr  40433  4atexlemex6  40444  ldilco  40486  ltrneq  40519  trlval2  40533  trlnidat  40543  cdlemd2  40569  cdlemd7  40574  cdlemd8  40575  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme11c  40631  cdleme11e  40633  cdleme11l  40639  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme15c  40646  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme16e  40652  cdleme16f  40653  cdleme0nex  40660  cdleme18d  40665  cdleme19b  40674  cdleme19d  40676  cdleme19e  40677  cdleme20f  40684  cdleme20i  40687  cdleme20k  40689  cdleme20l1  40690  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme21a  40695  cdleme21b  40696  cdleme21ct  40699  cdleme21d  40700  cdleme21e  40701  cdleme21f  40702  cdleme21h  40704  cdleme22eALTN  40715  cdleme22f2  40717  cdleme22g  40718  cdleme26e  40729  cdleme26eALTN  40731  cdleme26fALTN  40732  cdleme26f  40733  cdleme26f2ALTN  40734  cdleme26f2  40735  cdleme28a  40740  cdleme28b  40741  cdleme28  40743  cdleme29ex  40744  cdleme29c  40746  cdlemefrs29cpre1  40768  cdlemefr29exN  40772  cdlemefr32sn2aw  40774  cdlemefr29bpre0N  40776  cdlemefr29clN  40777  cdlemefr32fvaN  40779  cdlemefr32fva1  40780  cdlemefs32sn1aw  40784  cdleme43fsv1snlem  40790  cdleme41sn3a  40803  cdleme32fva  40807  cdleme32b  40812  cdleme32d  40814  cdleme32e  40815  cdleme32f  40816  cdleme32le  40817  cdleme35a  40818  cdleme35fnpq  40819  cdleme35b  40820  cdleme35c  40821  cdleme35d  40822  cdleme35e  40823  cdleme35f  40824  cdleme36a  40830  cdleme36m  40831  cdleme37m  40832  cdleme39a  40835  cdleme39n  40836  cdleme40m  40837  cdleme40n  40838  cdleme42e  40849  cdleme42f  40850  cdleme42g  40851  cdleme43bN  40860  cdleme43cN  40861  cdleme43dN  40862  cdleme46f2g2  40863  cdleme46f2g1  40864  cdleme17d2  40865  cdleme48b  40873  cdleme4gfv  40877  cdlemeg49le  40881  cdlemeg46c  40883  cdlemeg46fvaw  40886  cdlemeg46nlpq  40887  cdlemeg46frv  40895  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemeg46gfre  40902  cdleme50trn1  40919  cdleme50trn2a  40920  cdleme50trn2  40921  cdleme  40930  cdlemf  40933  trlord  40939  cdlemg2ce  40962  cdlemg7fvbwN  40977  cdlemg7aN  40995  cdlemg10bALTN  41006  cdlemg10a  41010  cdlemg10  41011  cdlemg12d  41016  cdlemg12f  41018  cdlemg12g  41019  cdlemg12  41020  cdlemg13a  41021  cdlemg13  41022  cdlemg17b  41032  cdlemg17dN  41033  cdlemg17dALTN  41034  cdlemg17e  41035  cdlemg17f  41036  cdlemg17g  41037  cdlemg17h  41038  cdlemg17i  41039  cdlemg17pq  41042  cdlemg17bq  41043  cdlemg17iqN  41044  cdlemg17  41047  cdlemg18d  41051  cdlemg18  41052  cdlemg19a  41053  cdlemg19  41054  cdlemg21  41056  cdlemg27a  41062  cdlemg28a  41063  cdlemg31b0N  41064  cdlemg27b  41066  cdlemg33b0  41071  cdlemg28b  41073  cdlemg28  41074  cdlemg33a  41076  cdlemg33  41081  cdlemg34  41082  cdlemg35  41083  cdlemg36  41084  ltrnco  41089  trlcone  41098  cdlemg44  41103  cdlemg47  41106  cdlemg48  41107  tendococl  41142  tendoplcl  41151  cdlemh1  41185  cdlemi  41190  cdlemj1  41191  cdlemj2  41192  tendocan  41194  cdlemk6  41207  cdlemki  41211  cdlemksat  41216  cdlemksv2  41217  cdlemk7  41218  cdlemk11  41219  cdlemk12  41220  cdlemkoatnle  41221  cdlemkole  41223  cdlemk14  41224  cdlemk15  41225  cdlemk16a  41226  cdlemk16  41227  cdlemk17  41228  cdlemk1u  41229  cdlemk5u  41231  cdlemk6u  41232  cdlemkuat  41236  cdlemk18  41238  cdlemk19  41239  cdlemk12u  41242  cdlemk21N  41243  cdlemk20  41244  cdlemkoatnle-2N  41245  cdlemk13-2N  41246  cdlemkole-2N  41247  cdlemk14-2N  41248  cdlemk15-2N  41249  cdlemk16-2N  41250  cdlemk17-2N  41251  cdlemk18-2N  41256  cdlemk19-2N  41257  cdlemk7u-2N  41258  cdlemk11u-2N  41259  cdlemk12u-2N  41260  cdlemk21-2N  41261  cdlemk20-2N  41262  cdlemk22  41263  cdlemk23-3  41272  cdlemk25-3  41274  cdlemk26b-3  41275  cdlemk27-3  41277  cdlemk28-3  41278  cdlemk33N  41279  cdlemk37  41284  cdlemky  41296  cdlemk11ta  41299  cdlemkid3N  41303  cdlemk11tc  41315  cdlemk11t  41316  cdlemk45  41317  cdlemk46  41318  cdlemk47  41319  cdlemk48  41320  cdlemk49  41321  cdlemk50  41322  cdlemk51  41323  cdlemk52  41324  cdlemk55b  41330  cdlemkyyN  41332  cdlemk55u1  41335  cdlemk55u  41336  cdlemk39u1  41337  cdlemk39u  41338  cdlemk56  41341  cdleml3N  41348  cdleml4N  41349  cdlemm10N  41488  dihord1  41588  dihord2a  41589  dihord2b  41590  dihord10  41593  dihord11c  41594  dihord2pre  41595  dihord4  41628  dihord5apre  41632  dihmeetlem1N  41660  dihglbcpreN  41670  dihjatc1  41681  dihjatc3  41683  dihmeetlem13N  41689  dihmeetlem20N  41696  baerlem3lem2  42080  baerlem5alem2  42081  baerlem5blem2  42082  hdmap14lem11  42248  hdmap14lem12  42249  flt4lem5  43002  monotuz  43292  congmul  43318  congsub  43321  rpnnen3lem  43382  ntrclsiso  44417  ntrclskb  44419  ntrclsk3  44420  wessf1ornlem  45538  infleinf  45724  lincdifsn  48778  itsclc0yqe  49115  itsclc0xyqsolr  49123  iscnrm3rlem8  49300  iscnrm3llem2  49303