Theorem simp23 1227

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

Assertion

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

Proof of Theorem simp23

Step	Hyp	Ref	Expression
1		simp3 1156	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant2 1152	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  simp123  1326  simp223  1335  simp323  1344  omeulem1  8568  elfiun  9391  ttrclselem2  9696  cofsmo  10254  modexp  14276  iscatd2  17738  funcoppc  17933  funcres  17954  catcisolem  18168  1stfcl  18254  2ndfcl  18255  prfcl  18260  evlfcl  18279  curf1cl  18285  curfcl  18289  hofcl  18316  pmtrprfv3  19525  ogrpsub  20208  ogrpsublt  20213  mdetunilem3  22752  mdetunilem4  22753  mdetuni0  22759  mdetmul  22761  prdsxmetlem  24506  isosctrlem3  26966  isosctr  26967  noinfbnd2lem1  27875  addsass  28179  f1otrg  29201  colinearalg  29241  ax5seglem6  29265  ax5seg  29269  axpasch  29272  axeuclid  29294  uhgr2edg  29539  clwwlkccat  30322  rhmdvd  33625  bnj966  35313  bnj967  35314  mclspps  36057  cgrtr  36465  cgrtr3  36467  ofscom  36480  btwnxfr  36529  colinearxfr  36548  lineext  36549  brofs2  36550  brifs2  36551  fscgr  36553  linecgr  36554  btwnconn1lem1  36560  btwnconn1lem2  36561  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem5  36564  btwnconn1lem6  36565  btwnconn1lem7  36566  seglecgr12im  36583  seglecgr12  36584  segletr  36587  broutsideof3  36599  outsideofeq  36603  lineunray  36620  eqlkr  39854  omlmod1i2N  40015  cvrcmp2  40039  cvlexch2  40084  cvlexchb2  40086  cvlatexchb2  40090  cvlatexch1  40091  cvlatexch2  40092  cvlatexch3  40093  cvlsupr7  40103  cvlsupr8  40104  atnlej1  40134  atnlej2  40135  2llnneN  40164  cvratlem  40176  atcvrneN  40185  atcvrj1  40186  atlelt  40193  2atjm  40200  3noncolr2  40204  3noncolr1N  40205  hlatcon2  40207  3dimlem2  40214  3dim1  40222  3dim2  40223  1cvrat  40231  ps-1  40232  ps-2  40233  2atjlej  40234  hlatexch3N  40235  ps-2b  40237  3atlem1  40238  3atlem2  40239  3atlem6  40243  llnle  40273  2atm  40282  ps-2c  40283  lplni2  40292  lplnle  40295  lplnnle2at  40296  lplnri3N  40310  llncvrlpln2  40312  2atmat  40316  2llnjaN  40321  2llnm2N  40323  2llnm4  40325  2llnmeqat  40326  lvolnle3at  40337  4atlem0ae  40349  4atlem0be  40350  4atlem3b  40353  4atlem9  40358  4atlem10a  40359  4atlem10  40361  4atlem11a  40362  4atlem12a  40365  4at  40368  4at2  40369  lplncvrlvol2  40370  2lplnm2N  40376  2llnma1b  40541  2llnma1  40542  2llnma3r  40543  2llnma2  40544  2llnma2rN  40545  cdlema1N  40546  cdlema2N  40547  paddasslem2  40576  paddasslem15  40589  paddasslem16  40590  pmodlem1  40601  pmod2iN  40604  hlmod1i  40611  atmod2i1  40616  atmod2i2  40617  atmod3i1  40619  atmod3i2  40620  atmod4i1  40621  atmod4i2  40622  llnexchb2  40624  dalawlem3  40628  dalawlem4  40629  dalawlem5  40630  dalawlem6  40631  dalawlem7  40632  dalawlem8  40633  dalawlem9  40634  dalawlem11  40636  dalawlem13  40638  dalawlem15  40640  osumcllem7N  40717  osumcllem9N  40719  osumcllem11N  40721  pl42lem1N  40734  4atex  40831  4atex2-0aOLDN  40833  4atex2-0bOLDN  40834  4atex2-0cOLDN  40835  trlval4  40943  cdlemc5  40950  cdlemd5  40957  cdlemd6  40958  cdleme00a  40964  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme4  40993  cdleme4a  40994  cdleme16aN  41014  cdleme11c  41016  cdleme11g  41020  cdleme11h  41021  cdleme12  41026  cdleme0nex  41045  cdleme18a  41046  cdleme18b  41047  cdleme18c  41048  cdleme18d  41050  cdleme20zN  41056  cdleme20y  41057  cdleme19a  41058  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20aN  41064  cdleme20c  41066  cdleme20d  41067  cdleme20i  41072  cdleme20j  41073  cdleme20l1  41075  cdleme20l2  41076  cdleme20m  41078  cdleme21b  41081  cdleme21c  41082  cdleme21j  41091  cdleme22aa  41094  cdleme22a  41095  cdleme22eALTN  41100  cdleme26e  41114  cdleme26fALTN  41117  cdleme26f  41118  cdleme26f2ALTN  41119  cdleme26f2  41120  cdleme27N  41124  cdleme28a  41125  cdleme28b  41126  cdleme30a  41133  cdlemefs45eN  41186  cdleme32c  41198  cdleme32e  41200  cdleme35h  41211  cdleme36a  41215  cdleme36m  41216  cdleme37m  41217  cdleme41sn3aw  41229  cdleme41sn4aw  41230  cdleme41fva11  41232  cdleme42k  41239  cdleme43cN  41246  cdleme43dN  41247  cdleme46f2g1  41249  cdlemeg47rv2  41265  cdlemeg46sfg  41275  cdlemeg46fjgN  41276  cdlemeg46rjgN  41277  cdlemeg46fjv  41278  cdlemeg46frv  41280  cdlemeg46vrg  41282  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemeg46gfv  41285  cdleme50trn2a  41305  cdlemg2fv2  41355  cdlemg4a  41363  cdlemg4e  41369  cdlemg4f  41370  cdlemg8b  41383  cdlemg8c  41384  cdlemg9a  41387  cdlemg9b  41388  cdlemg9  41389  cdlemg10a  41395  cdlemg12a  41398  cdlemg12b  41399  cdlemg12c  41400  cdlemg12  41405  cdlemg17dN  41418  cdlemg17dALTN  41419  cdlemg17e  41420  cdlemg17i  41424  cdlemg17ir  41425  cdlemg17pq  41427  cdlemg17bq  41428  cdlemg17iqN  41429  cdlemg17  41432  cdlemg18b  41434  cdlemg18c  41435  cdlemg18d  41436  cdlemg18  41437  cdlemg19  41439  cdlemg21  41441  cdlemg28a  41448  cdlemg31b0a  41450  cdlemg33b0  41456  cdlemg35  41468  cdlemg44a  41486  cdlemh  41572  cdlemi2  41574  cdlemj1  41576  cdlemk5a  41590  cdlemk5  41591  cdlemki  41596  cdlemkvcl  41597  cdlemk10  41598  cdlemksv2  41602  cdlemk7  41603  cdlemk11  41604  cdlemk12  41605  cdlemk15  41610  cdlemk16a  41611  cdlemk16  41612  cdlemk5u  41616  cdlemk6u  41617  cdlemk18  41623  cdlemk19  41624  cdlemk7u  41625  cdlemk11u  41626  cdlemk12u  41627  cdlemk21N  41628  cdlemk20  41629  cdlemkoatnle-2N  41630  cdlemk13-2N  41631  cdlemkole-2N  41632  cdlemk14-2N  41633  cdlemk15-2N  41634  cdlemk16-2N  41635  cdlemk17-2N  41636  cdlemk18-2N  41641  cdlemk19-2N  41642  cdlemk22  41648  cdlemk30  41649  cdlemk28-3  41663  cdlemk33N  41664  cdlemkfid1N  41676  cdlemkid1  41677  cdlemky  41681  cdlemk11ta  41684  cdlemk35s-id  41693  cdlemk39s-id  41695  cdlemk47  41704  cdlemk48  41705  cdlemk49  41706  cdlemk50  41707  cdlemk51  41708  cdlemk52  41709  cdlemk53a  41710  cdlemk53b  41711  cdlemk53  41712  cdlemk54  41713  cdlemk55a  41714  cdlemkyyN  41717  cdlemk43N  41718  cdlemk55u1  41720  cdlemk55u  41721  cdlemk39u1  41722  cdlemk19u1  41724  cdleml1N  41731  cdleml2N  41732  cdleml3N  41733  dia2dimlem6  41824  cdlemn2  41950  cdlemn2a  41951  cdlemn5pre  41955  cdlemn11pre  41965  dihjustlem  41971  dihjust  41972  dihmeetlem15N  42076  lclkrlem2y  42286  relexpxpnnidm  44412  ormkglobd  47574  natglobalincr  47576  iscnrm3llem1  49710  iscnrm3l  49712  swapffunc  50043  fucofunc  50120