Theorem simp11 1202

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 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1132	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  1301  simp211  1310  simp311  1319  omeulem1  8618  omeu  8621  ackbij1lem16  10271  coprimeprodsq  16841  pythagtriplem14  16861  pythagtrip  16867  mrelatglb  18617  subglsm  19705  lsmpropd  19709  mdetmul  22644  decpmatid  22791  isfil2  23879  filuni  23908  cxple2a  26755  isosctr  26878  nolesgn2o  27730  nolesgn2ores  27731  nogesgn1o  27732  nogesgn1ores  27733  nolt02o  27754  nogt01o  27755  sslttr  27866  cofcut2  27970  brbtwn2  28934  colinearalg  28939  ax5seglem3  28960  clwwlknonex2  30137  measres  34202  bayesth  34420  ofscom  35988  btwndiff  36008  ifscgr  36025  brofs2  36058  brifs2  36059  fscgr  36061  btwnconn1lem1  36068  btwnconn1lem2  36069  btwnconn1lem3  36070  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem7  36074  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn1lem12  36079  seglecgr12im  36091  seglecgr12  36092  ivthALT  36317  eqlkr  39080  lkrshp  39086  lshpkrlem5  39095  cvrval3  39395  4noncolr3  39435  4noncolr2  39436  4noncolr1  39437  athgt  39438  3dimlem2  39441  3dimlem3a  39442  3dimlem4a  39445  3dimlem4  39446  3dimlem4OLDN  39447  3dim2  39450  1cvratex  39455  hlatexch4  39463  ps-2b  39464  3atlem1  39465  3atlem2  39466  3atlem4  39468  3atlem5  39469  3atlem6  39470  llnnleat  39495  2atm  39509  ps-2c  39510  llnmlplnN  39521  lplnnlelln  39525  2atmat  39543  2llnjN  39549  lvoli2  39563  lvolnlelln  39566  4atlem3b  39580  4atlem9  39585  4atlem10a  39586  4atlem10  39588  4atlem11a  39589  4atlem11b  39590  4atlem12a  39592  4atlem12b  39593  4at  39595  4at2  39596  lplncvrlvol2  39597  2lplnj  39602  dalemswapyz  39638  dath2  39719  lneq2at  39760  2lnat  39766  cdlema1N  39773  cdlemb  39776  paddasslem15  39816  pmodlem1  39828  llnmod2i2  39845  llnexchb2lem  39850  llnexchb2  39851  dalawlem1  39853  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem10  39862  dalawlem11  39863  dalawlem12  39864  dalawlem13  39865  dalawlem15  39867  dalaw  39868  osumcllem5N  39942  osumcllem6N  39943  osumcllem7N  39944  osumcllem9N  39946  osumcllem10N  39947  osumcllem11N  39948  pl42lem1N  39961  lhpexle3lem  39993  lhpmcvr5N  40009  lhp2atne  40016  lhp2at0ne  40018  4atexlemswapqr  40045  4atexlemex6  40056  ldilco  40098  ltrneq  40131  trlval2  40145  trlnidat  40155  cdlemd2  40181  cdlemd7  40186  cdlemd8  40187  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme11c  40243  cdleme11e  40245  cdleme11l  40251  cdleme11  40252  cdleme14  40255  cdleme15a  40256  cdleme15c  40258  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme0nex  40272  cdleme18d  40277  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20f  40296  cdleme20i  40299  cdleme20k  40301  cdleme20l1  40302  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21a  40307  cdleme21b  40308  cdleme21ct  40311  cdleme21d  40312  cdleme21e  40313  cdleme21f  40314  cdleme21h  40316  cdleme22eALTN  40327  cdleme22f2  40329  cdleme22g  40330  cdleme26e  40341  cdleme26eALTN  40343  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme28a  40352  cdleme28b  40353  cdleme28  40355  cdleme29ex  40356  cdleme29c  40358  cdlemefrs29cpre1  40380  cdlemefr29exN  40384  cdlemefr32sn2aw  40386  cdlemefr29bpre0N  40388  cdlemefr29clN  40389  cdlemefr32fvaN  40391  cdlemefr32fva1  40392  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme41sn3a  40415  cdleme32fva  40419  cdleme32b  40424  cdleme32d  40426  cdleme32e  40427  cdleme32f  40428  cdleme32le  40429  cdleme35a  40430  cdleme35fnpq  40431  cdleme35b  40432  cdleme35c  40433  cdleme35d  40434  cdleme35e  40435  cdleme35f  40436  cdleme36a  40442  cdleme36m  40443  cdleme37m  40444  cdleme39a  40447  cdleme39n  40448  cdleme40m  40449  cdleme40n  40450  cdleme42e  40461  cdleme42f  40462  cdleme42g  40463  cdleme43bN  40472  cdleme43cN  40473  cdleme43dN  40474  cdleme46f2g2  40475  cdleme46f2g1  40476  cdleme17d2  40477  cdleme48b  40485  cdleme4gfv  40489  cdlemeg49le  40493  cdlemeg46c  40495  cdlemeg46fvaw  40498  cdlemeg46nlpq  40499  cdlemeg46frv  40507  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfre  40514  cdleme50trn1  40531  cdleme50trn2a  40532  cdleme50trn2  40533  cdleme  40542  cdlemf  40545  trlord  40551  cdlemg2ce  40574  cdlemg7fvbwN  40589  cdlemg7aN  40607  cdlemg10bALTN  40618  cdlemg10a  40622  cdlemg10  40623  cdlemg12d  40628  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg13  40634  cdlemg17b  40644  cdlemg17dN  40645  cdlemg17dALTN  40646  cdlemg17e  40647  cdlemg17f  40648  cdlemg17g  40649  cdlemg17h  40650  cdlemg17i  40651  cdlemg17pq  40654  cdlemg17bq  40655  cdlemg17iqN  40656  cdlemg17  40659  cdlemg18d  40663  cdlemg18  40664  cdlemg19a  40665  cdlemg19  40666  cdlemg21  40668  cdlemg27a  40674  cdlemg28a  40675  cdlemg31b0N  40676  cdlemg27b  40678  cdlemg33b0  40683  cdlemg28b  40685  cdlemg28  40686  cdlemg33a  40688  cdlemg33  40693  cdlemg34  40694  cdlemg35  40695  cdlemg36  40696  ltrnco  40701  trlcone  40710  cdlemg44  40715  cdlemg47  40718  cdlemg48  40719  tendococl  40754  tendoplcl  40763  cdlemh1  40797  cdlemi  40802  cdlemj1  40803  cdlemj2  40804  tendocan  40806  cdlemk6  40819  cdlemki  40823  cdlemksat  40828  cdlemksv2  40829  cdlemk7  40830  cdlemk11  40831  cdlemk12  40832  cdlemkoatnle  40833  cdlemkole  40835  cdlemk14  40836  cdlemk15  40837  cdlemk16a  40838  cdlemk16  40839  cdlemk17  40840  cdlemk1u  40841  cdlemk5u  40843  cdlemk6u  40844  cdlemkuat  40848  cdlemk18  40850  cdlemk19  40851  cdlemk12u  40854  cdlemk21N  40855  cdlemk20  40856  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk7u-2N  40870  cdlemk11u-2N  40871  cdlemk12u-2N  40872  cdlemk21-2N  40873  cdlemk20-2N  40874  cdlemk22  40875  cdlemk23-3  40884  cdlemk25-3  40886  cdlemk26b-3  40887  cdlemk27-3  40889  cdlemk28-3  40890  cdlemk33N  40891  cdlemk37  40896  cdlemky  40908  cdlemk11ta  40911  cdlemkid3N  40915  cdlemk11tc  40927  cdlemk11t  40928  cdlemk45  40929  cdlemk46  40930  cdlemk47  40931  cdlemk48  40932  cdlemk49  40933  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  cdlemk55b  40942  cdlemkyyN  40944  cdlemk55u1  40947  cdlemk55u  40948  cdlemk39u1  40949  cdlemk39u  40950  cdlemk56  40953  cdleml3N  40960  cdleml4N  40961  cdlemm10N  41100  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord10  41205  dihord11c  41206  dihord2pre  41207  dihord4  41240  dihord5apre  41244  dihmeetlem1N  41272  dihglbcpreN  41282  dihjatc1  41293  dihjatc3  41295  dihmeetlem13N  41301  dihmeetlem20N  41308  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  hdmap14lem11  41860  hdmap14lem12  41861  flt4lem5  42636  monotuz  42929  congmul  42955  congsub  42958  rpnnen3lem  43019  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  wessf1ornlem  45127  infleinf  45321  lincdifsn  48269  itsclc0yqe  48610  itsclc0xyqsolr  48618  iscnrm3rlem8  48743  iscnrm3llem2  48746