Theorem simp21 1207

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp21	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp21

Step	Hyp	Ref	Expression
1		simp1 1136	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1134	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:  simp121  1306  simp221  1315  simp321  1324  omeulem1  8492  cofsmo  10155  axdc4lem  10341  0catg  17589  funcoppc  17777  funcres  17798  catcisolem  18012  1stfcl  18098  2ndfcl  18099  prfcl  18104  evlfcl  18123  curf1cl  18129  curfcl  18133  hofcl  18160  mulgdirlem  19013  ogrpsub  20044  ogrpaddlt  20045  ogrpsublt  20049  mdetunilem4  22525  mdetuni0  22531  mdetmul  22533  prdsxmetlem  24278  isosctrlem3  26752  isosctr  26753  amgmlem  26922  nosupbnd2lem1  27649  addsass  27943  f1otrg  28844  colinearalg  28883  ax5seglem6  28907  ax5seg  28911  axpasch  28914  axeuclidlem  28935  axeuclid  28936  uhgr2edg  29181  numclwlk1lem2  30342  rhmdvd  33281  bnj1128  34994  mclspps  35620  cgrtr  36026  cgrtr3  36028  ofscom  36041  segconeq  36044  ifscgr  36078  btwnxfr  36090  colinearxfr  36109  lineext  36110  brofs2  36111  brifs2  36112  fscgr  36114  linecgr  36115  btwnconn1lem1  36121  btwnconn1lem2  36122  btwnconn1lem3  36123  btwnconn1lem4  36124  btwnconn1lem5  36125  btwnconn1lem6  36126  btwnconn1lem7  36127  seglecgr12im  36144  seglecgr12  36145  segletr  36148  broutsideof3  36160  outsideofeq  36164  lineunray  36181  lineelsb2  36182  linecom  36184  lshpkrlem5  39153  omlmod1i2N  39299  cvrnbtwn3  39315  cvrcmp  39322  cvrcmp2  39323  cvlexch2  39368  cvlexchb2  39370  cvlatexchb2  39374  cvlatexch2  39376  cvlatexch3  39377  cvlsupr7  39387  atnlej1  39418  atnlej2  39419  2llnneN  39448  cvratlem  39460  atcvrneN  39469  atcvrj1  39470  atlelt  39477  2atjm  39484  3noncolr2  39488  3noncolr1N  39489  3dimlem2  39498  3dim1  39506  3dim2  39507  1cvrat  39515  ps-1  39516  ps-2  39517  2atjlej  39518  hlatexch3N  39519  ps-2b  39521  3atlem1  39522  3atlem2  39523  3atlem5  39526  3atlem6  39527  llnle  39557  2atm  39566  ps-2c  39567  lplni2  39576  lplnle  39579  lplnnle2at  39580  lplnri3N  39594  llncvrlpln2  39596  2atmat  39600  2llnm2N  39607  2llnm4  39609  2llnmeqat  39610  lvolnle3at  39621  4atlem0ae  39633  4atlem0be  39634  4atlem3b  39637  4atlem9  39642  4atlem10a  39643  4atlem10  39645  4atlem11a  39646  4atlem12a  39649  4at2  39653  2lplnm2N  39660  lneq2at  39817  2llnma1b  39825  2llnma1  39826  2llnma3r  39827  2llnma2  39828  2llnma2rN  39829  cdlema1N  39830  paddasslem2  39860  paddasslem15  39873  paddasslem16  39874  pmodlem1  39885  pmodlem2  39886  pmod2iN  39888  hlmod1i  39895  atmod1i1m  39897  atmod2i1  39900  atmod2i2  39901  atmod3i1  39903  atmod3i2  39904  atmod4i1  39905  atmod4i2  39906  llnexchb2lem  39907  llnexch2N  39909  dalawlem3  39912  dalawlem4  39913  dalawlem5  39914  dalawlem6  39915  dalawlem7  39916  dalawlem8  39917  dalawlem9  39918  dalawlem11  39920  dalawlem12  39921  dalawlem13  39922  dalawlem15  39924  osumcllem9N  40003  pl42lem1N  40018  4atexlems  40091  4atex2  40116  4atex2-0bOLDN  40118  trlval4  40227  cdlemc5  40234  cdlemc6  40235  cdlemd2  40238  cdlemd4  40240  cdlemd6  40242  cdleme00a  40248  cdleme0e  40256  cdleme3g  40273  cdleme3h  40274  cdleme3  40276  cdleme4  40277  cdleme4a  40278  cdleme5  40279  cdleme9  40292  cdleme16aN  40298  cdleme11c  40300  cdleme11e  40302  cdleme11g  40304  cdleme11h  40305  cdleme11j  40306  cdleme11k  40307  cdleme11l  40308  cdleme11  40309  cdleme12  40310  cdleme14  40312  cdleme15c  40315  cdleme16b  40318  cdleme16c  40319  cdleme16d  40320  cdleme16e  40321  cdleme16f  40322  cdleme0nex  40329  cdleme18a  40330  cdleme18c  40332  cdleme18d  40334  cdlemednpq  40338  cdlemednuN  40339  cdleme20zN  40340  cdleme20y  40341  cdleme19a  40342  cdleme19b  40343  cdleme19d  40345  cdleme19e  40346  cdleme20aN  40348  cdleme20bN  40349  cdleme20c  40350  cdleme20d  40351  cdleme20f  40353  cdleme20g  40354  cdleme20i  40356  cdleme20j  40357  cdleme20l1  40359  cdleme20l2  40360  cdleme20l  40361  cdleme20m  40362  cdleme21b  40365  cdleme21c  40366  cdleme21e  40370  cdleme21f  40371  cdleme22a  40379  cdleme22b  40380  cdleme22e  40383  cdleme22eALTN  40384  cdleme22f  40385  cdleme26eALTN  40400  cdleme26fALTN  40401  cdleme26f  40402  cdleme26f2ALTN  40403  cdleme26f2  40404  cdleme27N  40408  cdleme28a  40409  cdleme28b  40410  cdleme30a  40417  cdleme43fsv1snlem  40459  cdlemefs31fv1  40463  cdlemefs45eN  40470  cdleme32b  40481  cdleme32c  40482  cdleme32d  40483  cdleme35h  40495  cdleme36a  40499  cdleme36m  40500  cdleme37m  40501  cdleme40m  40506  cdleme40n  40507  cdleme41sn3aw  40513  cdleme41sn4aw  40514  cdleme41fva11  40516  cdleme42k  40523  cdleme43cN  40530  cdleme43dN  40531  cdleme46f2g1  40533  cdlemeg47rv2  40549  cdlemeg46sfg  40559  cdlemeg46fjgN  40560  cdlemeg46rjgN  40561  cdlemeg46fjv  40562  cdlemeg46frv  40564  cdlemeg46vrg  40566  cdlemeg46rgv  40567  cdlemeg46req  40568  cdlemeg46gfv  40569  cdlemg4a  40647  cdlemg4d  40652  cdlemg4e  40653  cdlemg4f  40654  cdlemg4g  40655  cdlemg4  40656  cdlemg6d  40660  cdlemg6e  40661  cdlemg8b  40667  cdlemg8c  40668  cdlemg9a  40671  cdlemg9b  40672  cdlemg10a  40679  cdlemg10  40680  cdlemg12a  40682  cdlemg12b  40683  cdlemg12f  40687  cdlemg12g  40688  cdlemg12  40689  cdlemg17dN  40702  cdlemg17dALTN  40703  cdlemg17e  40704  cdlemg17f  40705  cdlemg17g  40706  cdlemg17h  40707  cdlemg17i  40708  cdlemg17pq  40711  cdlemg17iqN  40713  cdlemg17  40716  cdlemg18b  40718  cdlemg18c  40719  cdlemg19a  40722  cdlemg19  40723  cdlemg28a  40732  cdlemg27b  40735  cdlemg28b  40742  cdlemg28  40743  cdlemg33a  40745  cdlemg33b  40746  cdlemg33c  40747  cdlemg33d  40748  cdlemg33e  40749  cdlemg33  40750  cdlemg35  40752  cdlemg36  40753  cdlemg44a  40770  cdlemh  40856  cdlemi2  40858  cdlemj1  40860  tendocan  40863  cdlemk5a  40874  cdlemki  40880  cdlemkvcl  40881  cdlemk10  40882  cdlemksv2  40886  cdlemkole  40892  cdlemk14  40893  cdlemk15  40894  cdlemk16a  40895  cdlemk16  40896  cdlemk17  40897  cdlemk18  40907  cdlemk19  40908  cdlemkoatnle-2N  40914  cdlemk13-2N  40915  cdlemkole-2N  40916  cdlemk14-2N  40917  cdlemk15-2N  40918  cdlemk16-2N  40919  cdlemk17-2N  40920  cdlemk18-2N  40925  cdlemk19-2N  40926  cdlemk30  40933  cdlemk18-3N  40939  cdlemk23-3  40941  cdlemk25-3  40943  cdlemk27-3  40946  cdlemk37  40953  cdlemkfid1N  40960  cdlemkid1  40961  cdlemky  40965  cdlemk11ta  40968  cdlemk47  40988  cdlemk48  40989  cdlemk49  40990  cdlemk50  40991  cdlemk51  40992  cdlemk52  40993  cdlemk53a  40994  cdlemk54  40997  cdlemk39u1  41006  cdlemk19u1  41008  cdleml1N  41015  cdleml2N  41016  cdleml3N  41017  dia2dimlem6  41108  cdlemn2  41234  cdlemn2a  41235  cdlemn5pre  41239  cdlemn10  41245  cdlemn11c  41248  cdlemn11pre  41249  dihjustlem  41255  dihjust  41256  lclkrlem2y  41570  aks6d1c1  42149  relexpmulnn  43742  ormkglobd  46913  natglobalincr  46915  lincreslvec3  48514  iscnrm3llem1  48980  iscnrm3l  48982  swapffunc  49314  fucofunc  49391  amgmwlem  49834