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 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  1303  simp211  1312  simp311  1321  omeulem1  8620  omeu  8623  ackbij1lem16  10274  coprimeprodsq  16846  pythagtriplem14  16866  pythagtrip  16872  mrelatglb  18605  subglsm  19691  lsmpropd  19695  mdetmul  22629  decpmatid  22776  isfil2  23864  filuni  23893  cxple2a  26741  isosctr  26864  nolesgn2o  27716  nolesgn2ores  27717  nogesgn1o  27718  nogesgn1ores  27719  nolt02o  27740  nogt01o  27741  sslttr  27852  cofcut2  27956  brbtwn2  28920  colinearalg  28925  ax5seglem3  28946  clwwlknonex2  30128  measres  34223  bayesth  34441  ofscom  36008  btwndiff  36028  ifscgr  36045  brofs2  36078  brifs2  36079  fscgr  36081  btwnconn1lem1  36088  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem7  36094  btwnconn1lem8  36095  btwnconn1lem9  36096  btwnconn1lem10  36097  btwnconn1lem11  36098  btwnconn1lem12  36099  seglecgr12im  36111  seglecgr12  36112  ivthALT  36336  eqlkr  39100  lkrshp  39106  lshpkrlem5  39115  cvrval3  39415  4noncolr3  39455  4noncolr2  39456  4noncolr1  39457  athgt  39458  3dimlem2  39461  3dimlem3a  39462  3dimlem4a  39465  3dimlem4  39466  3dimlem4OLDN  39467  3dim2  39470  1cvratex  39475  hlatexch4  39483  ps-2b  39484  3atlem1  39485  3atlem2  39486  3atlem4  39488  3atlem5  39489  3atlem6  39490  llnnleat  39515  2atm  39529  ps-2c  39530  llnmlplnN  39541  lplnnlelln  39545  2atmat  39563  2llnjN  39569  lvoli2  39583  lvolnlelln  39586  4atlem3b  39600  4atlem9  39605  4atlem10a  39606  4atlem10  39608  4atlem11a  39609  4atlem11b  39610  4atlem12a  39612  4atlem12b  39613  4at  39615  4at2  39616  lplncvrlvol2  39617  2lplnj  39622  dalemswapyz  39658  dath2  39739  lneq2at  39780  2lnat  39786  cdlema1N  39793  cdlemb  39796  paddasslem15  39836  pmodlem1  39848  llnmod2i2  39865  llnexchb2lem  39870  llnexchb2  39871  dalawlem1  39873  dalawlem3  39875  dalawlem4  39876  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem9  39881  dalawlem10  39882  dalawlem11  39883  dalawlem12  39884  dalawlem13  39885  dalawlem15  39887  dalaw  39888  osumcllem5N  39962  osumcllem6N  39963  osumcllem7N  39964  osumcllem9N  39966  osumcllem10N  39967  osumcllem11N  39968  pl42lem1N  39981  lhpexle3lem  40013  lhpmcvr5N  40029  lhp2atne  40036  lhp2at0ne  40038  4atexlemswapqr  40065  4atexlemex6  40076  ldilco  40118  ltrneq  40151  trlval2  40165  trlnidat  40175  cdlemd2  40201  cdlemd7  40206  cdlemd8  40207  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme11c  40263  cdleme11e  40265  cdleme11l  40271  cdleme11  40272  cdleme14  40275  cdleme15a  40276  cdleme15c  40278  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme0nex  40292  cdleme18d  40297  cdleme19b  40306  cdleme19d  40308  cdleme19e  40309  cdleme20f  40316  cdleme20i  40319  cdleme20k  40321  cdleme20l1  40322  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21a  40327  cdleme21b  40328  cdleme21ct  40331  cdleme21d  40332  cdleme21e  40333  cdleme21f  40334  cdleme21h  40336  cdleme22eALTN  40347  cdleme22f2  40349  cdleme22g  40350  cdleme26e  40361  cdleme26eALTN  40363  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme28a  40372  cdleme28b  40373  cdleme28  40375  cdleme29ex  40376  cdleme29c  40378  cdlemefrs29cpre1  40400  cdlemefr29exN  40404  cdlemefr32sn2aw  40406  cdlemefr29bpre0N  40408  cdlemefr29clN  40409  cdlemefr32fvaN  40411  cdlemefr32fva1  40412  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme41sn3a  40435  cdleme32fva  40439  cdleme32b  40444  cdleme32d  40446  cdleme32e  40447  cdleme32f  40448  cdleme32le  40449  cdleme35a  40450  cdleme35fnpq  40451  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35e  40455  cdleme35f  40456  cdleme36a  40462  cdleme36m  40463  cdleme37m  40464  cdleme39a  40467  cdleme39n  40468  cdleme40m  40469  cdleme40n  40470  cdleme42e  40481  cdleme42f  40482  cdleme42g  40483  cdleme43bN  40492  cdleme43cN  40493  cdleme43dN  40494  cdleme46f2g2  40495  cdleme46f2g1  40496  cdleme17d2  40497  cdleme48b  40505  cdleme4gfv  40509  cdlemeg49le  40513  cdlemeg46c  40515  cdlemeg46fvaw  40518  cdlemeg46nlpq  40519  cdlemeg46frv  40527  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemeg46gfre  40534  cdleme50trn1  40551  cdleme50trn2a  40552  cdleme50trn2  40553  cdleme  40562  cdlemf  40565  trlord  40571  cdlemg2ce  40594  cdlemg7fvbwN  40609  cdlemg7aN  40627  cdlemg10bALTN  40638  cdlemg10a  40642  cdlemg10  40643  cdlemg12d  40648  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg13  40654  cdlemg17b  40664  cdlemg17dN  40665  cdlemg17dALTN  40666  cdlemg17e  40667  cdlemg17f  40668  cdlemg17g  40669  cdlemg17h  40670  cdlemg17i  40671  cdlemg17pq  40674  cdlemg17bq  40675  cdlemg17iqN  40676  cdlemg17  40679  cdlemg18d  40683  cdlemg18  40684  cdlemg19a  40685  cdlemg19  40686  cdlemg21  40688  cdlemg27a  40694  cdlemg28a  40695  cdlemg31b0N  40696  cdlemg27b  40698  cdlemg33b0  40703  cdlemg28b  40705  cdlemg28  40706  cdlemg33a  40708  cdlemg33  40713  cdlemg34  40714  cdlemg35  40715  cdlemg36  40716  ltrnco  40721  trlcone  40730  cdlemg44  40735  cdlemg47  40738  cdlemg48  40739  tendococl  40774  tendoplcl  40783  cdlemh1  40817  cdlemi  40822  cdlemj1  40823  cdlemj2  40824  tendocan  40826  cdlemk6  40839  cdlemki  40843  cdlemksat  40848  cdlemksv2  40849  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemkoatnle  40853  cdlemkole  40855  cdlemk14  40856  cdlemk15  40857  cdlemk16a  40858  cdlemk16  40859  cdlemk17  40860  cdlemk1u  40861  cdlemk5u  40863  cdlemk6u  40864  cdlemkuat  40868  cdlemk18  40870  cdlemk19  40871  cdlemk12u  40874  cdlemk21N  40875  cdlemk20  40876  cdlemkoatnle-2N  40877  cdlemk13-2N  40878  cdlemkole-2N  40879  cdlemk14-2N  40880  cdlemk15-2N  40881  cdlemk16-2N  40882  cdlemk17-2N  40883  cdlemk18-2N  40888  cdlemk19-2N  40889  cdlemk7u-2N  40890  cdlemk11u-2N  40891  cdlemk12u-2N  40892  cdlemk21-2N  40893  cdlemk20-2N  40894  cdlemk22  40895  cdlemk23-3  40904  cdlemk25-3  40906  cdlemk26b-3  40907  cdlemk27-3  40909  cdlemk28-3  40910  cdlemk33N  40911  cdlemk37  40916  cdlemky  40928  cdlemk11ta  40931  cdlemkid3N  40935  cdlemk11tc  40947  cdlemk11t  40948  cdlemk45  40949  cdlemk46  40950  cdlemk47  40951  cdlemk48  40952  cdlemk49  40953  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  cdlemk55b  40962  cdlemkyyN  40964  cdlemk55u1  40967  cdlemk55u  40968  cdlemk39u1  40969  cdlemk39u  40970  cdlemk56  40973  cdleml3N  40980  cdleml4N  40981  cdlemm10N  41120  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord10  41225  dihord11c  41226  dihord2pre  41227  dihord4  41260  dihord5apre  41264  dihmeetlem1N  41292  dihglbcpreN  41302  dihjatc1  41313  dihjatc3  41315  dihmeetlem13N  41321  dihmeetlem20N  41328  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  hdmap14lem11  41880  hdmap14lem12  41881  flt4lem5  42660  monotuz  42953  congmul  42979  congsub  42982  rpnnen3lem  43043  ntrclsiso  44080  ntrclskb  44082  ntrclsk3  44083  wessf1ornlem  45190  infleinf  45383  lincdifsn  48341  itsclc0yqe  48682  itsclc0xyqsolr  48690  iscnrm3rlem8  48844  iscnrm3llem2  48847