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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp123  1326  simp223  1335  simp323  1344  omeulem1  8594  elfiun  9426  ttrclselem2  9731  cofsmo  10351  modexp  14386  iscatd2  17861  funcoppc  18056  funcres  18077  catcisolem  18291  1stfcl  18377  2ndfcl  18378  prfcl  18383  evlfcl  18402  curf1cl  18408  curfcl  18412  hofcl  18439  pmtrprfv3  19674  ogrpsub  20357  ogrpsublt  20362  mdetunilem3  22935  mdetunilem4  22936  mdetuni0  22942  mdetmul  22944  prdsxmetlem  24693  isosctrlem3  27154  isosctr  27155  noinfbnd2lem1  28093  addsass  28397  f1otrg  29454  colinearalg  29494  ax5seglem6  29518  ax5seg  29522  axpasch  29525  axeuclid  29547  uhgr2edg  29795  clwwlkccat  30587  rhmdvd  33932  bnj966  35621  bnj967  35622  mclspps  36436  cgrtr  36850  cgrtr3  36852  ofscom  36865  btwnxfr  36914  colinearxfr  36933  lineext  36934  brofs2  36935  brifs2  36936  fscgr  36938  linecgr  36939  btwnconn1lem1  36945  btwnconn1lem2  36946  btwnconn1lem3  36947  btwnconn1lem4  36948  btwnconn1lem5  36949  btwnconn1lem6  36950  btwnconn1lem7  36951  seglecgr12im  36968  seglecgr12  36969  segletr  36972  broutsideof3  36984  outsideofeq  36988  lineunray  37005  eqlkr  40250  omlmod1i2N  40411  cvrcmp2  40435  cvlexch2  40480  cvlexchb2  40482  cvlatexchb2  40486  cvlatexch1  40487  cvlatexch2  40488  cvlatexch3  40489  cvlsupr7  40499  cvlsupr8  40500  atnlej1  40530  atnlej2  40531  2llnneN  40560  cvratlem  40572  atcvrneN  40581  atcvrj1  40582  atlelt  40589  2atjm  40596  3noncolr2  40600  3noncolr1N  40601  hlatcon2  40603  3dimlem2  40610  3dim1  40618  3dim2  40619  1cvrat  40627  ps-1  40628  ps-2  40629  2atjlej  40630  hlatexch3N  40631  ps-2b  40633  3atlem1  40634  3atlem2  40635  3atlem6  40639  llnle  40669  2atm  40678  ps-2c  40679  lplni2  40688  lplnle  40691  lplnnle2at  40692  lplnri3N  40706  llncvrlpln2  40708  2atmat  40712  2llnjaN  40717  2llnm2N  40719  2llnm4  40721  2llnmeqat  40722  lvolnle3at  40733  4atlem0ae  40745  4atlem0be  40746  4atlem3b  40749  4atlem9  40754  4atlem10a  40755  4atlem10  40757  4atlem11a  40758  4atlem12a  40761  4at  40764  4at2  40765  lplncvrlvol2  40766  2lplnm2N  40772  2llnma1b  40937  2llnma1  40938  2llnma3r  40939  2llnma2  40940  2llnma2rN  40941  cdlema1N  40942  cdlema2N  40943  paddasslem2  40972  paddasslem15  40985  paddasslem16  40986  pmodlem1  40997  pmod2iN  41000  hlmod1i  41007  atmod2i1  41012  atmod2i2  41013  atmod3i1  41015  atmod3i2  41016  atmod4i1  41017  atmod4i2  41018  llnexchb2  41020  dalawlem3  41024  dalawlem4  41025  dalawlem5  41026  dalawlem6  41027  dalawlem7  41028  dalawlem8  41029  dalawlem9  41030  dalawlem11  41032  dalawlem13  41034  dalawlem15  41036  osumcllem7N  41113  osumcllem9N  41115  osumcllem11N  41117  pl42lem1N  41130  4atex  41227  4atex2-0aOLDN  41229  4atex2-0bOLDN  41230  4atex2-0cOLDN  41231  trlval4  41339  cdlemc5  41346  cdlemd5  41353  cdlemd6  41354  cdleme00a  41360  cdleme3g  41385  cdleme3h  41386  cdleme3  41388  cdleme4  41389  cdleme4a  41390  cdleme16aN  41410  cdleme11c  41412  cdleme11g  41416  cdleme11h  41417  cdleme12  41422  cdleme0nex  41441  cdleme18a  41442  cdleme18b  41443  cdleme18c  41444  cdleme18d  41446  cdleme20zN  41452  cdleme20y  41453  cdleme19a  41454  cdleme19b  41455  cdleme19d  41457  cdleme19e  41458  cdleme20aN  41460  cdleme20c  41462  cdleme20d  41463  cdleme20i  41468  cdleme20j  41469  cdleme20l1  41471  cdleme20l2  41472  cdleme20m  41474  cdleme21b  41477  cdleme21c  41478  cdleme21j  41487  cdleme22aa  41490  cdleme22a  41491  cdleme22eALTN  41496  cdleme26e  41510  cdleme26fALTN  41513  cdleme26f  41514  cdleme26f2ALTN  41515  cdleme26f2  41516  cdleme27N  41520  cdleme28a  41521  cdleme28b  41522  cdleme30a  41529  cdlemefs45eN  41582  cdleme32c  41594  cdleme32e  41596  cdleme35h  41607  cdleme36a  41611  cdleme36m  41612  cdleme37m  41613  cdleme41sn3aw  41625  cdleme41sn4aw  41626  cdleme41fva11  41628  cdleme42k  41635  cdleme43cN  41642  cdleme43dN  41643  cdleme46f2g1  41645  cdlemeg47rv2  41661  cdlemeg46sfg  41671  cdlemeg46fjgN  41672  cdlemeg46rjgN  41673  cdlemeg46fjv  41674  cdlemeg46frv  41676  cdlemeg46vrg  41678  cdlemeg46rgv  41679  cdlemeg46req  41680  cdlemeg46gfv  41681  cdleme50trn2a  41701  cdlemg2fv2  41751  cdlemg4a  41759  cdlemg4e  41765  cdlemg4f  41766  cdlemg8b  41779  cdlemg8c  41780  cdlemg9a  41783  cdlemg9b  41784  cdlemg9  41785  cdlemg10a  41791  cdlemg12a  41794  cdlemg12b  41795  cdlemg12c  41796  cdlemg12  41801  cdlemg17dN  41814  cdlemg17dALTN  41815  cdlemg17e  41816  cdlemg17i  41820  cdlemg17ir  41821  cdlemg17pq  41823  cdlemg17bq  41824  cdlemg17iqN  41825  cdlemg17  41828  cdlemg18b  41830  cdlemg18c  41831  cdlemg18d  41832  cdlemg18  41833  cdlemg19  41835  cdlemg21  41837  cdlemg28a  41844  cdlemg31b0a  41846  cdlemg33b0  41852  cdlemg35  41864  cdlemg44a  41882  cdlemh  41968  cdlemi2  41970  cdlemj1  41972  cdlemk5a  41986  cdlemk5  41987  cdlemki  41992  cdlemkvcl  41993  cdlemk10  41994  cdlemksv2  41998  cdlemk7  41999  cdlemk11  42000  cdlemk12  42001  cdlemk15  42006  cdlemk16a  42007  cdlemk16  42008  cdlemk5u  42012  cdlemk6u  42013  cdlemk18  42019  cdlemk19  42020  cdlemk7u  42021  cdlemk11u  42022  cdlemk12u  42023  cdlemk21N  42024  cdlemk20  42025  cdlemkoatnle-2N  42026  cdlemk13-2N  42027  cdlemkole-2N  42028  cdlemk14-2N  42029  cdlemk15-2N  42030  cdlemk16-2N  42031  cdlemk17-2N  42032  cdlemk18-2N  42037  cdlemk19-2N  42038  cdlemk22  42044  cdlemk30  42045  cdlemk28-3  42059  cdlemk33N  42060  cdlemkfid1N  42072  cdlemkid1  42073  cdlemky  42077  cdlemk11ta  42080  cdlemk35s-id  42089  cdlemk39s-id  42091  cdlemk47  42100  cdlemk48  42101  cdlemk49  42102  cdlemk50  42103  cdlemk51  42104  cdlemk52  42105  cdlemk53a  42106  cdlemk53b  42107  cdlemk53  42108  cdlemk54  42109  cdlemk55a  42110  cdlemkyyN  42113  cdlemk43N  42114  cdlemk55u1  42116  cdlemk55u  42117  cdlemk39u1  42118  cdlemk19u1  42120  cdleml1N  42127  cdleml2N  42128  cdleml3N  42129  dia2dimlem6  42220  cdlemn2  42346  cdlemn2a  42347  cdlemn5pre  42351  cdlemn11pre  42361  dihjustlem  42367  dihjust  42368  dihmeetlem15N  42472  lclkrlem2y  42682  relexpxpnnidm  44797  ormkglobd  47981  iscnrm3llem1  50157  iscnrm3l  50159  swapffunc  50498  fucofunc  50575  parmapfunc2  50868  parmapfunc  50869