Theorem simp22 1203

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

Assertion

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

Proof of Theorem simp22

Step	Hyp	Ref	Expression
1		simp2 1133	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant2 1130	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp122  1302  simp222  1311  simp322  1320  elfiun  8894  cofsmo  9691  modexp  13600  funcoppc  17145  funcres  17166  catcisolem  17366  1stfcl  17447  2ndfcl  17448  prfcl  17453  evlfcl  17472  curf1cl  17478  curfcl  17482  hofcl  17509  mulgdirlem  18258  pmtrprfv3  18582  mdetunilem4  21224  mdetuni0  21230  mdetmul  21232  prdsxmetlem  22978  isosctrlem3  25398  isosctr  25399  amgmlem  25567  f1otrg  26657  colinearalg  26696  ax5seglem6  26720  ax5seg  26724  axpasch  26727  axeuclidlem  26748  axeuclid  26749  ogrpsub  30717  ogrpaddlt  30718  ogrpsublt  30722  rhmdvd  30894  bnj966  32216  mclspps  32831  cgrtr  33453  cgrtr3  33455  ofscom  33468  cgrextend  33469  btwnxfr  33517  colinearxfr  33536  lineext  33537  fscgr  33541  linecgr  33542  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem7  33554  seglecgr12im  33571  seglecgr12  33572  segletr  33575  broutsideof3  33587  outsideofeq  33591  lineunray  33608  linecom  33611  eqlkr  36250  lshpkrlem5  36265  omlmod1i2N  36411  cvrnbtwn3  36427  cvrcmp2  36435  cvlexch2  36480  cvlexchb2  36482  cvlatexchb2  36486  cvlatexch1  36487  cvlatexch2  36488  cvlatexch3  36489  cvlsupr7  36499  cvlsupr8  36500  atnlej1  36530  atnlej2  36531  2llnneN  36560  cvratlem  36572  atcvrneN  36581  atlelt  36589  2atjm  36596  3noncolr2  36600  3noncolr1N  36601  hlatcon2  36603  3dimlem2  36610  3dim1  36618  3dim2  36619  1cvrat  36627  ps-1  36628  ps-2  36629  2atjlej  36630  hlatexch3N  36631  ps-2b  36633  3atlem1  36634  3atlem5  36638  3atlem6  36639  2atm  36678  ps-2c  36679  lplni2  36688  lplnri3N  36706  llncvrlpln2  36708  2atmat  36712  2llnm2N  36719  2llnm3N  36720  2llnm4  36721  2llnmeqat  36722  lvolnle3at  36733  4atlem0ae  36745  4atlem0be  36746  4atlem3b  36749  4atlem9  36754  4atlem10a  36755  4atlem10  36757  4atlem11a  36758  4atlem12a  36761  4at2  36765  2lplnm2N  36772  lneq2at  36929  2llnma1b  36937  2llnma1  36938  2llnma3r  36939  2llnma2  36940  2llnma2rN  36941  cdlema1N  36942  paddasslem2  36972  paddasslem16  36986  pmodlem1  36997  pmod2iN  37000  hlmod1i  37007  atmod2i1  37012  atmod2i2  37013  atmod3i1  37015  atmod3i2  37016  atmod4i1  37017  atmod4i2  37018  llnexchb2lem  37019  llnexch2N  37021  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem13  37034  dalawlem15  37036  osumcllem7N  37113  osumcllem9N  37115  pl42lem1N  37130  4atexlemswapqr  37214  4atex2  37228  4atex2-0bOLDN  37230  trlval4  37339  cdlemc5  37346  cdlemc6  37347  cdlemd2  37350  cdlemd4  37352  cdlemd6  37354  cdleme00a  37360  cdleme0e  37368  cdleme4  37389  cdleme4a  37390  cdleme5  37391  cdleme9  37404  cdleme16aN  37410  cdleme11c  37412  cdleme11dN  37413  cdleme11e  37414  cdleme11g  37416  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme11l  37420  cdleme11  37421  cdleme12  37422  cdleme13  37423  cdleme14  37424  cdleme15a  37425  cdleme15c  37427  cdleme16b  37430  cdleme16c  37431  cdleme16d  37432  cdleme16e  37433  cdleme16f  37434  cdleme17d1  37440  cdleme0nex  37441  cdleme18a  37442  cdleme18b  37443  cdleme18c  37444  cdleme18d  37446  cdlemednpq  37450  cdlemednuN  37451  cdleme20zN  37452  cdleme20y  37453  cdleme19a  37454  cdleme19b  37455  cdleme19d  37457  cdleme19e  37458  cdleme20aN  37460  cdleme20d  37463  cdleme20f  37465  cdleme20g  37466  cdleme20i  37468  cdleme20j  37469  cdleme20l1  37471  cdleme20l2  37472  cdleme20l  37473  cdleme20m  37474  cdleme21b  37477  cdleme21c  37478  cdleme21e  37482  cdleme21j  37487  cdleme22aa  37490  cdleme22a  37491  cdleme22b  37492  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme26fALTN  37513  cdleme26f  37514  cdleme26f2ALTN  37515  cdleme26f2  37516  cdleme27N  37520  cdleme28a  37521  cdleme28b  37522  cdleme30a  37529  cdlemefs31fv1  37575  cdleme32b  37593  cdleme32c  37594  cdleme32e  37596  cdleme35h  37607  cdleme36a  37611  cdleme36m  37612  cdleme41sn3aw  37625  cdleme41sn4aw  37626  cdleme41fva11  37628  cdleme42k  37635  cdleme43cN  37642  cdleme46f2g1  37645  cdlemeg46fjgN  37672  cdlemeg46fjv  37674  cdlemeg46frv  37676  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemeg46gfv  37681  cdleme50trn2a  37701  cdlemg4a  37759  cdlemg4d  37764  cdlemg4e  37765  cdlemg4f  37766  cdlemg8c  37780  cdlemg9a  37783  cdlemg9b  37784  cdlemg10a  37791  cdlemg10  37792  cdlemg12b  37795  cdlemg12f  37799  cdlemg12g  37800  cdlemg12  37801  cdlemg17dN  37814  cdlemg17dALTN  37815  cdlemg17e  37816  cdlemg17f  37817  cdlemg17g  37818  cdlemg17i  37820  cdlemg17ir  37821  cdlemg17pq  37823  cdlemg17bq  37824  cdlemg17iqN  37825  cdlemg17  37828  cdlemg18b  37830  cdlemg18c  37831  cdlemg18d  37832  cdlemg18  37833  cdlemg19  37835  cdlemg21  37837  cdlemg28a  37844  cdlemg31b0a  37846  cdlemg27b  37847  cdlemg33b0  37852  cdlemg28b  37854  cdlemg28  37855  cdlemg35  37864  cdlemg36  37865  cdlemg44a  37882  cdlemh  37968  cdlemi2  37970  cdlemj1  37972  tendocan  37975  cdlemk5a  37986  cdlemk5  37987  cdlemki  37992  cdlemkvcl  37993  cdlemk10  37994  cdlemksv2  37998  cdlemk7  37999  cdlemk11  38000  cdlemk12  38001  cdlemkoatnle  38002  cdlemk15  38006  cdlemk16a  38007  cdlemk16  38008  cdlemk1u  38010  cdlemk5u  38012  cdlemk6u  38013  cdlemk18  38019  cdlemk19  38020  cdlemk7u  38021  cdlemk11u  38022  cdlemk12u  38023  cdlemk21N  38024  cdlemk20  38025  cdlemkoatnle-2N  38026  cdlemk13-2N  38027  cdlemkole-2N  38028  cdlemk14-2N  38029  cdlemk15-2N  38030  cdlemk16-2N  38031  cdlemk17-2N  38032  cdlemk18-2N  38037  cdlemk19-2N  38038  cdlemk22  38044  cdlemk30  38045  cdlemkuel-3  38049  cdlemkuv2-3N  38050  cdlemk18-3N  38051  cdlemkfid1N  38072  cdlemkid1  38073  cdlemkfid3N  38076  cdlemky  38077  cdlemk11ta  38080  cdlemk47  38100  cdlemk48  38101  cdlemk49  38102  cdlemk50  38103  cdlemk51  38104  cdlemk52  38105  cdlemk53a  38106  cdlemk53  38108  cdlemk54  38109  cdlemk55a  38110  cdlemkyyN  38113  cdlemk43N  38114  cdlemk55u1  38116  cdlemk55u  38117  cdlemk39u1  38118  cdlemk19u1  38120  cdleml1N  38127  cdleml2N  38128  cdleml3N  38129  dia2dimlem6  38220  cdlemn2  38346  cdlemn2a  38347  cdlemn5pre  38351  cdlemn11a  38358  dihjustlem  38367  dihjust  38368  dihmeetlem15N  38472  lclkrlem2y  38682  relexpmulnn  40074  amgmwlem  44923