Theorem simp23 1209

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 1138	. 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:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8546  elfiun  9381  ttrclselem2  9679  cofsmo  10222  modexp  14203  iscatd2  17642  funcoppc  17837  funcres  17858  catcisolem  18072  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  pmtrprfv3  19384  mdetunilem3  22501  mdetunilem4  22502  mdetuni0  22508  mdetmul  22510  prdsxmetlem  24256  isosctrlem3  26730  isosctr  26731  noinfbnd2lem1  27642  addsass  27912  f1otrg  28798  colinearalg  28837  ax5seglem6  28861  ax5seg  28865  axpasch  28868  axeuclid  28890  uhgr2edg  29135  clwwlkccat  29919  ogrpsub  33030  ogrpsublt  33035  rhmdvd  33296  bnj966  34934  bnj967  34935  mclspps  35571  cgrtr  35980  cgrtr3  35982  ofscom  35995  btwnxfr  36044  colinearxfr  36063  lineext  36064  brofs2  36065  brifs2  36066  fscgr  36068  linecgr  36069  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem7  36081  seglecgr12im  36098  seglecgr12  36099  segletr  36102  broutsideof3  36114  outsideofeq  36118  lineunray  36135  eqlkr  39092  omlmod1i2N  39253  cvrcmp2  39277  cvlexch2  39322  cvlexchb2  39324  cvlatexchb2  39328  cvlatexch1  39329  cvlatexch2  39330  cvlatexch3  39331  cvlsupr7  39341  cvlsupr8  39342  atnlej1  39373  atnlej2  39374  2llnneN  39403  cvratlem  39415  atcvrneN  39424  atcvrj1  39425  atlelt  39432  2atjm  39439  3noncolr2  39443  3noncolr1N  39444  hlatcon2  39446  3dimlem2  39453  3dim1  39461  3dim2  39462  1cvrat  39470  ps-1  39471  ps-2  39472  2atjlej  39473  hlatexch3N  39474  ps-2b  39476  3atlem1  39477  3atlem2  39478  3atlem6  39482  llnle  39512  2atm  39521  ps-2c  39522  lplni2  39531  lplnle  39534  lplnnle2at  39535  lplnri3N  39549  llncvrlpln2  39551  2atmat  39555  2llnjaN  39560  2llnm2N  39562  2llnm4  39564  2llnmeqat  39565  lvolnle3at  39576  4atlem0ae  39588  4atlem0be  39589  4atlem3b  39592  4atlem9  39597  4atlem10a  39598  4atlem10  39600  4atlem11a  39601  4atlem12a  39604  4at  39607  4at2  39608  lplncvrlvol2  39609  2lplnm2N  39615  2llnma1b  39780  2llnma1  39781  2llnma3r  39782  2llnma2  39783  2llnma2rN  39784  cdlema1N  39785  cdlema2N  39786  paddasslem2  39815  paddasslem15  39828  paddasslem16  39829  pmodlem1  39840  pmod2iN  39843  hlmod1i  39850  atmod2i1  39855  atmod2i2  39856  atmod3i1  39858  atmod3i2  39859  atmod4i1  39860  atmod4i2  39861  llnexchb2  39863  dalawlem3  39867  dalawlem4  39868  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem9  39873  dalawlem11  39875  dalawlem13  39877  dalawlem15  39879  osumcllem7N  39956  osumcllem9N  39958  osumcllem11N  39960  pl42lem1N  39973  4atex  40070  4atex2-0aOLDN  40072  4atex2-0bOLDN  40073  4atex2-0cOLDN  40074  trlval4  40182  cdlemc5  40189  cdlemd5  40196  cdlemd6  40197  cdleme00a  40203  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4  40232  cdleme4a  40233  cdleme16aN  40253  cdleme11c  40255  cdleme11g  40259  cdleme11h  40260  cdleme12  40265  cdleme0nex  40284  cdleme18a  40285  cdleme18b  40286  cdleme18c  40287  cdleme18d  40289  cdleme20zN  40295  cdleme20y  40296  cdleme19a  40297  cdleme19b  40298  cdleme19d  40300  cdleme19e  40301  cdleme20aN  40303  cdleme20c  40305  cdleme20d  40306  cdleme20i  40311  cdleme20j  40312  cdleme20l1  40314  cdleme20l2  40315  cdleme20m  40317  cdleme21b  40320  cdleme21c  40321  cdleme21j  40330  cdleme22aa  40333  cdleme22a  40334  cdleme22eALTN  40339  cdleme26e  40353  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme27N  40363  cdleme28a  40364  cdleme28b  40365  cdleme30a  40372  cdlemefs45eN  40425  cdleme32c  40437  cdleme32e  40439  cdleme35h  40450  cdleme36a  40454  cdleme36m  40455  cdleme37m  40456  cdleme41sn3aw  40468  cdleme41sn4aw  40469  cdleme41fva11  40471  cdleme42k  40478  cdleme43cN  40485  cdleme43dN  40486  cdleme46f2g1  40488  cdlemeg47rv2  40504  cdlemeg46sfg  40514  cdlemeg46fjgN  40515  cdlemeg46rjgN  40516  cdlemeg46fjv  40517  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemeg46gfv  40524  cdleme50trn2a  40544  cdlemg2fv2  40594  cdlemg4a  40602  cdlemg4e  40608  cdlemg4f  40609  cdlemg8b  40622  cdlemg8c  40623  cdlemg9a  40626  cdlemg9b  40627  cdlemg9  40628  cdlemg10a  40634  cdlemg12a  40637  cdlemg12b  40638  cdlemg12c  40639  cdlemg12  40644  cdlemg17dN  40657  cdlemg17dALTN  40658  cdlemg17e  40659  cdlemg17i  40663  cdlemg17ir  40664  cdlemg17pq  40666  cdlemg17bq  40667  cdlemg17iqN  40668  cdlemg17  40671  cdlemg18b  40673  cdlemg18c  40674  cdlemg18d  40675  cdlemg18  40676  cdlemg19  40678  cdlemg21  40680  cdlemg28a  40687  cdlemg31b0a  40689  cdlemg33b0  40695  cdlemg35  40707  cdlemg44a  40725  cdlemh  40811  cdlemi2  40813  cdlemj1  40815  cdlemk5a  40829  cdlemk5  40830  cdlemki  40835  cdlemkvcl  40836  cdlemk10  40837  cdlemksv2  40841  cdlemk7  40842  cdlemk11  40843  cdlemk12  40844  cdlemk15  40849  cdlemk16a  40850  cdlemk16  40851  cdlemk5u  40855  cdlemk6u  40856  cdlemk18  40862  cdlemk19  40863  cdlemk7u  40864  cdlemk11u  40865  cdlemk12u  40866  cdlemk21N  40867  cdlemk20  40868  cdlemkoatnle-2N  40869  cdlemk13-2N  40870  cdlemkole-2N  40871  cdlemk14-2N  40872  cdlemk15-2N  40873  cdlemk16-2N  40874  cdlemk17-2N  40875  cdlemk18-2N  40880  cdlemk19-2N  40881  cdlemk22  40887  cdlemk30  40888  cdlemk28-3  40902  cdlemk33N  40903  cdlemkfid1N  40915  cdlemkid1  40916  cdlemky  40920  cdlemk11ta  40923  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk47  40943  cdlemk48  40944  cdlemk49  40945  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  cdlemk53a  40949  cdlemk53b  40950  cdlemk53  40951  cdlemk54  40952  cdlemk55a  40953  cdlemkyyN  40956  cdlemk43N  40957  cdlemk55u1  40959  cdlemk55u  40960  cdlemk39u1  40961  cdlemk19u1  40963  cdleml1N  40970  cdleml2N  40971  cdleml3N  40972  dia2dimlem6  41063  cdlemn2  41189  cdlemn2a  41190  cdlemn5pre  41194  cdlemn11pre  41204  dihjustlem  41210  dihjust  41211  dihmeetlem15N  41315  lclkrlem2y  41525  relexpxpnnidm  43692  ormkglobd  46873  natglobalincr  46875  iscnrm3llem1  48937  iscnrm3l  48939  swapffunc  49271  fucofunc  49348