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 1139	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant2 1135	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp123  1308  simp223  1317  simp323  1326  omeulem1  8578  elfiun  9421  ttrclselem2  9717  cofsmo  10260  modexp  14197  iscatd2  17621  funcoppc  17821  funcres  17842  catcisolem  18056  1stfcl  18145  2ndfcl  18146  prfcl  18151  evlfcl  18171  curf1cl  18177  curfcl  18181  hofcl  18208  pmtrprfv3  19315  mdetunilem3  22098  mdetunilem4  22099  mdetuni0  22105  mdetmul  22107  prdsxmetlem  23856  isosctrlem3  26305  isosctr  26306  noinfbnd2lem1  27213  addsass  27468  f1otrg  28102  colinearalg  28148  ax5seglem6  28172  ax5seg  28176  axpasch  28179  axeuclid  28201  uhgr2edg  28445  clwwlkccat  29223  ogrpsub  32212  ogrpsublt  32217  rhmdvd  32405  bnj966  33893  bnj967  33894  mclspps  34513  cgrtr  34902  cgrtr3  34904  ofscom  34917  btwnxfr  34966  colinearxfr  34985  lineext  34986  brofs2  34987  brifs2  34988  fscgr  34990  linecgr  34991  btwnconn1lem1  34997  btwnconn1lem2  34998  btwnconn1lem3  34999  btwnconn1lem4  35000  btwnconn1lem5  35001  btwnconn1lem6  35002  btwnconn1lem7  35003  seglecgr12im  35020  seglecgr12  35021  segletr  35024  broutsideof3  35036  outsideofeq  35040  lineunray  35057  eqlkr  37907  omlmod1i2N  38068  cvrcmp2  38092  cvlexch2  38137  cvlexchb2  38139  cvlatexchb2  38143  cvlatexch1  38144  cvlatexch2  38145  cvlatexch3  38146  cvlsupr7  38156  cvlsupr8  38157  atnlej1  38188  atnlej2  38189  2llnneN  38218  cvratlem  38230  atcvrneN  38239  atcvrj1  38240  atlelt  38247  2atjm  38254  3noncolr2  38258  3noncolr1N  38259  hlatcon2  38261  3dimlem2  38268  3dim1  38276  3dim2  38277  1cvrat  38285  ps-1  38286  ps-2  38287  2atjlej  38288  hlatexch3N  38289  ps-2b  38291  3atlem1  38292  3atlem2  38293  3atlem6  38297  llnle  38327  2atm  38336  ps-2c  38337  lplni2  38346  lplnle  38349  lplnnle2at  38350  lplnri3N  38364  llncvrlpln2  38366  2atmat  38370  2llnjaN  38375  2llnm2N  38377  2llnm4  38379  2llnmeqat  38380  lvolnle3at  38391  4atlem0ae  38403  4atlem0be  38404  4atlem3b  38407  4atlem9  38412  4atlem10a  38413  4atlem10  38415  4atlem11a  38416  4atlem12a  38419  4at  38422  4at2  38423  lplncvrlvol2  38424  2lplnm2N  38430  2llnma1b  38595  2llnma1  38596  2llnma3r  38597  2llnma2  38598  2llnma2rN  38599  cdlema1N  38600  cdlema2N  38601  paddasslem2  38630  paddasslem15  38643  paddasslem16  38644  pmodlem1  38655  pmod2iN  38658  hlmod1i  38665  atmod2i1  38670  atmod2i2  38671  atmod3i1  38673  atmod3i2  38674  atmod4i1  38675  atmod4i2  38676  llnexchb2  38678  dalawlem3  38682  dalawlem4  38683  dalawlem5  38684  dalawlem6  38685  dalawlem7  38686  dalawlem8  38687  dalawlem9  38688  dalawlem11  38690  dalawlem13  38692  dalawlem15  38694  osumcllem7N  38771  osumcllem9N  38773  osumcllem11N  38775  pl42lem1N  38788  4atex  38885  4atex2-0aOLDN  38887  4atex2-0bOLDN  38888  4atex2-0cOLDN  38889  trlval4  38997  cdlemc5  39004  cdlemd5  39011  cdlemd6  39012  cdleme00a  39018  cdleme3g  39043  cdleme3h  39044  cdleme3  39046  cdleme4  39047  cdleme4a  39048  cdleme16aN  39068  cdleme11c  39070  cdleme11g  39074  cdleme11h  39075  cdleme12  39080  cdleme0nex  39099  cdleme18a  39100  cdleme18b  39101  cdleme18c  39102  cdleme18d  39104  cdleme20zN  39110  cdleme20y  39111  cdleme19a  39112  cdleme19b  39113  cdleme19d  39115  cdleme19e  39116  cdleme20aN  39118  cdleme20c  39120  cdleme20d  39121  cdleme20i  39126  cdleme20j  39127  cdleme20l1  39129  cdleme20l2  39130  cdleme20m  39132  cdleme21b  39135  cdleme21c  39136  cdleme21j  39145  cdleme22aa  39148  cdleme22a  39149  cdleme22eALTN  39154  cdleme26e  39168  cdleme26fALTN  39171  cdleme26f  39172  cdleme26f2ALTN  39173  cdleme26f2  39174  cdleme27N  39178  cdleme28a  39179  cdleme28b  39180  cdleme30a  39187  cdlemefs45eN  39240  cdleme32c  39252  cdleme32e  39254  cdleme35h  39265  cdleme36a  39269  cdleme36m  39270  cdleme37m  39271  cdleme41sn3aw  39283  cdleme41sn4aw  39284  cdleme41fva11  39286  cdleme42k  39293  cdleme43cN  39300  cdleme43dN  39301  cdleme46f2g1  39303  cdlemeg47rv2  39319  cdlemeg46sfg  39329  cdlemeg46fjgN  39330  cdlemeg46rjgN  39331  cdlemeg46fjv  39332  cdlemeg46frv  39334  cdlemeg46vrg  39336  cdlemeg46rgv  39337  cdlemeg46req  39338  cdlemeg46gfv  39339  cdleme50trn2a  39359  cdlemg2fv2  39409  cdlemg4a  39417  cdlemg4e  39423  cdlemg4f  39424  cdlemg8b  39437  cdlemg8c  39438  cdlemg9a  39441  cdlemg9b  39442  cdlemg9  39443  cdlemg10a  39449  cdlemg12a  39452  cdlemg12b  39453  cdlemg12c  39454  cdlemg12  39459  cdlemg17dN  39472  cdlemg17dALTN  39473  cdlemg17e  39474  cdlemg17i  39478  cdlemg17ir  39479  cdlemg17pq  39481  cdlemg17bq  39482  cdlemg17iqN  39483  cdlemg17  39486  cdlemg18b  39488  cdlemg18c  39489  cdlemg18d  39490  cdlemg18  39491  cdlemg19  39493  cdlemg21  39495  cdlemg28a  39502  cdlemg31b0a  39504  cdlemg33b0  39510  cdlemg35  39522  cdlemg44a  39540  cdlemh  39626  cdlemi2  39628  cdlemj1  39630  cdlemk5a  39644  cdlemk5  39645  cdlemki  39650  cdlemkvcl  39651  cdlemk10  39652  cdlemksv2  39656  cdlemk7  39657  cdlemk11  39658  cdlemk12  39659  cdlemk15  39664  cdlemk16a  39665  cdlemk16  39666  cdlemk5u  39670  cdlemk6u  39671  cdlemk18  39677  cdlemk19  39678  cdlemk7u  39679  cdlemk11u  39680  cdlemk12u  39681  cdlemk21N  39682  cdlemk20  39683  cdlemkoatnle-2N  39684  cdlemk13-2N  39685  cdlemkole-2N  39686  cdlemk14-2N  39687  cdlemk15-2N  39688  cdlemk16-2N  39689  cdlemk17-2N  39690  cdlemk18-2N  39695  cdlemk19-2N  39696  cdlemk22  39702  cdlemk30  39703  cdlemk28-3  39717  cdlemk33N  39718  cdlemkfid1N  39730  cdlemkid1  39731  cdlemky  39735  cdlemk11ta  39738  cdlemk35s-id  39747  cdlemk39s-id  39749  cdlemk47  39758  cdlemk48  39759  cdlemk49  39760  cdlemk50  39761  cdlemk51  39762  cdlemk52  39763  cdlemk53a  39764  cdlemk53b  39765  cdlemk53  39766  cdlemk54  39767  cdlemk55a  39768  cdlemkyyN  39771  cdlemk43N  39772  cdlemk55u1  39774  cdlemk55u  39775  cdlemk39u1  39776  cdlemk19u1  39778  cdleml1N  39785  cdleml2N  39786  cdleml3N  39787  dia2dimlem6  39878  cdlemn2  40004  cdlemn2a  40005  cdlemn5pre  40009  cdlemn11pre  40019  dihjustlem  40025  dihjust  40026  dihmeetlem15N  40130  lclkrlem2y  40340  relexpxpnnidm  42387  natglobalincr  45526  iscnrm3llem1  47484  iscnrm3l  47486