Theorem simp21 1094

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

Assertion

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

Proof of Theorem simp21

Step	Hyp	Ref	Expression
1		simp1 1061	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1083	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl21  1139  simpr21  1148  simp121  1193  simp221  1202  simp321  1211  omeulem1  7662  cofsmo  9091  axdc4lem  9277  0catg  16348  funcoppc  16535  funcres  16556  catcisolem  16756  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  mulgdirlem  17572  mdetunilem4  20421  mdetuni0  20427  mdetmul  20429  prdsxmetlem  22173  isosctrlem3  24550  isosctr  24551  amgmlem  24716  f1otrg  25751  colinearalg  25790  ax5seglem6  25814  ax5seg  25818  axpasch  25821  axeuclidlem  25842  axeuclid  25843  uhgr2edg  26100  ogrpsub  29717  ogrpaddlt  29718  ogrpsublt  29722  rhmdvd  29821  bnj1128  31058  mclspps  31481  nosupbnd2lem1  31861  cgrtr  32099  cgrtr3  32101  ofscom  32114  segconeq  32117  ifscgr  32151  btwnxfr  32163  colinearxfr  32182  lineext  32183  brofs2  32184  brifs2  32185  fscgr  32187  linecgr  32188  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem7  32200  seglecgr12im  32217  seglecgr12  32218  segletr  32221  broutsideof3  32233  outsideofeq  32237  lineunray  32254  lineelsb2  32255  linecom  32257  lshpkrlem5  34401  omlmod1i2N  34547  cvrnbtwn3  34563  cvrcmp  34570  cvrcmp2  34571  cvlexch2  34616  cvlexchb2  34618  cvlatexchb2  34622  cvlatexch2  34624  cvlatexch3  34625  cvlsupr7  34635  atnlej1  34665  atnlej2  34666  2llnneN  34695  cvratlem  34707  atcvrneN  34716  atcvrj1  34717  atlelt  34724  2atjm  34731  3noncolr2  34735  3noncolr1N  34736  3dimlem2  34745  3dim1  34753  3dim2  34754  1cvrat  34762  ps-1  34763  ps-2  34764  2atjlej  34765  hlatexch3N  34766  ps-2b  34768  3atlem1  34769  3atlem2  34770  3atlem5  34773  3atlem6  34774  llnle  34804  2atm  34813  ps-2c  34814  lplni2  34823  lplnle  34826  lplnnle2at  34827  lplnri3N  34841  llncvrlpln2  34843  2atmat  34847  2llnm2N  34854  2llnm4  34856  2llnmeqat  34857  lvolnle3at  34868  4atlem0ae  34880  4atlem0be  34881  4atlem3b  34884  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem12a  34896  4at2  34900  2lplnm2N  34907  lneq2at  35064  2llnma1b  35072  2llnma1  35073  2llnma3r  35074  2llnma2  35075  2llnma2rN  35076  cdlema1N  35077  paddasslem2  35107  paddasslem15  35120  paddasslem16  35121  pmodlem1  35132  pmodlem2  35133  pmod2iN  35135  hlmod1i  35142  atmod1i1m  35144  atmod2i1  35147  atmod2i2  35148  atmod3i1  35150  atmod3i2  35151  atmod4i1  35152  atmod4i2  35153  llnexchb2lem  35154  llnexch2N  35156  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem13  35169  dalawlem15  35171  osumcllem9N  35250  pl42lem1N  35265  4atexlems  35338  4atex2  35363  4atex2-0bOLDN  35365  trlval4  35475  cdlemc5  35482  cdlemc6  35483  cdlemd2  35486  cdlemd4  35488  cdlemd6  35490  cdleme00a  35496  cdleme0e  35504  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4  35525  cdleme4a  35526  cdleme5  35527  cdleme9  35540  cdleme16aN  35546  cdleme11c  35548  cdleme11e  35550  cdleme11g  35552  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme11l  35556  cdleme11  35557  cdleme12  35558  cdleme14  35560  cdleme15c  35563  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme0nex  35577  cdleme18a  35578  cdleme18c  35580  cdleme18d  35582  cdlemednpq  35586  cdlemednuN  35587  cdleme20zN  35588  cdleme20y  35589  cdleme20yOLD  35590  cdleme19a  35591  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20aN  35597  cdleme20bN  35598  cdleme20c  35599  cdleme20d  35600  cdleme20f  35602  cdleme20g  35603  cdleme20i  35605  cdleme20j  35606  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21b  35614  cdleme21c  35615  cdleme21e  35619  cdleme21f  35620  cdleme22a  35628  cdleme22b  35629  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme26eALTN  35649  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme30a  35666  cdleme43fsv1snlem  35708  cdlemefs31fv1  35712  cdlemefs45eN  35719  cdleme32b  35730  cdleme32c  35731  cdleme32d  35732  cdleme35h  35744  cdleme36a  35748  cdleme36m  35749  cdleme37m  35750  cdleme40m  35755  cdleme40n  35756  cdleme41sn3aw  35762  cdleme41sn4aw  35763  cdleme41fva11  35765  cdleme42k  35772  cdleme43cN  35779  cdleme43dN  35780  cdleme46f2g1  35782  cdlemeg47rv2  35798  cdlemeg46sfg  35808  cdlemeg46fjgN  35809  cdlemeg46rjgN  35810  cdlemeg46fjv  35811  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfv  35818  cdlemg4a  35896  cdlemg4d  35901  cdlemg4e  35902  cdlemg4f  35903  cdlemg4g  35904  cdlemg4  35905  cdlemg6d  35909  cdlemg6e  35910  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg9b  35921  cdlemg10a  35928  cdlemg10  35929  cdlemg12a  35931  cdlemg12b  35932  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg17dN  35951  cdlemg17dALTN  35952  cdlemg17e  35953  cdlemg17f  35954  cdlemg17g  35955  cdlemg17h  35956  cdlemg17i  35957  cdlemg17pq  35960  cdlemg17iqN  35962  cdlemg17  35965  cdlemg18b  35967  cdlemg18c  35968  cdlemg19a  35971  cdlemg19  35972  cdlemg28a  35981  cdlemg27b  35984  cdlemg28b  35991  cdlemg28  35992  cdlemg33a  35994  cdlemg33b  35995  cdlemg33c  35996  cdlemg33d  35997  cdlemg33e  35998  cdlemg33  35999  cdlemg35  36001  cdlemg36  36002  cdlemg44a  36019  cdlemh  36105  cdlemi2  36107  cdlemj1  36109  tendocan  36112  cdlemk5a  36123  cdlemki  36129  cdlemkvcl  36130  cdlemk10  36131  cdlemksv2  36135  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk16a  36144  cdlemk16  36145  cdlemk17  36146  cdlemk18  36156  cdlemk19  36157  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk30  36182  cdlemk18-3N  36188  cdlemk23-3  36190  cdlemk25-3  36192  cdlemk27-3  36195  cdlemk37  36202  cdlemkfid1N  36209  cdlemkid1  36210  cdlemky  36214  cdlemk11ta  36217  cdlemk47  36237  cdlemk48  36238  cdlemk49  36239  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  cdlemk54  36246  cdlemk39u1  36255  cdlemk19u1  36257  cdleml1N  36264  cdleml2N  36265  cdleml3N  36266  dia2dimlem6  36358  cdlemn2  36484  cdlemn2a  36485  cdlemn5pre  36489  cdlemn10  36495  cdlemn11c  36498  cdlemn11pre  36499  dihjustlem  36505  dihjust  36506  lclkrlem2y  36820  relexpmulnn  38001  lincreslvec3  42271  amgmwlem  42548