MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp21 Structured version   Visualization version   GIF version

Theorem simp21 1249
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp21 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp21
StepHypRef Expression
1 simp1 1131 . 2 ((𝜓𝜒𝜃) → 𝜓)
213ad2ant2 1129 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  simpl21OLD  1322  simpr21OLD  1340  simp121  1390  simp221  1399  simp321  1408  omeulem1  7831  cofsmo  9283  axdc4lem  9469  0catg  16549  funcoppc  16736  funcres  16757  catcisolem  16957  1stfcl  17038  2ndfcl  17039  prfcl  17044  evlfcl  17063  curf1cl  17069  curfcl  17073  hofcl  17100  mulgdirlem  17773  mdetunilem4  20623  mdetuni0  20629  mdetmul  20631  prdsxmetlem  22374  isosctrlem3  24749  isosctr  24750  amgmlem  24915  f1otrg  25950  colinearalg  25989  ax5seglem6  26013  ax5seg  26017  axpasch  26020  axeuclidlem  26041  axeuclid  26042  uhgr2edg  26299  numclwlk1lem2  27531  ogrpsub  30026  ogrpaddlt  30027  ogrpsublt  30031  rhmdvd  30130  bnj1128  31365  mclspps  31788  nosupbnd2lem1  32167  cgrtr  32405  cgrtr3  32407  ofscom  32420  segconeq  32423  ifscgr  32457  btwnxfr  32469  colinearxfr  32488  lineext  32489  brofs2  32490  brifs2  32491  fscgr  32493  linecgr  32494  btwnconn1lem1  32500  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem4  32503  btwnconn1lem5  32504  btwnconn1lem6  32505  btwnconn1lem7  32506  seglecgr12im  32523  seglecgr12  32524  segletr  32527  broutsideof3  32539  outsideofeq  32543  lineunray  32560  lineelsb2  32561  linecom  32563  lshpkrlem5  34904  omlmod1i2N  35050  cvrnbtwn3  35066  cvrcmp  35073  cvrcmp2  35074  cvlexch2  35119  cvlexchb2  35121  cvlatexchb2  35125  cvlatexch2  35127  cvlatexch3  35128  cvlsupr7  35138  atnlej1  35168  atnlej2  35169  2llnneN  35198  cvratlem  35210  atcvrneN  35219  atcvrj1  35220  atlelt  35227  2atjm  35234  3noncolr2  35238  3noncolr1N  35239  3dimlem2  35248  3dim1  35256  3dim2  35257  1cvrat  35265  ps-1  35266  ps-2  35267  2atjlej  35268  hlatexch3N  35269  ps-2b  35271  3atlem1  35272  3atlem2  35273  3atlem5  35276  3atlem6  35277  llnle  35307  2atm  35316  ps-2c  35317  lplni2  35326  lplnle  35329  lplnnle2at  35330  lplnri3N  35344  llncvrlpln2  35346  2atmat  35350  2llnm2N  35357  2llnm4  35359  2llnmeqat  35360  lvolnle3at  35371  4atlem0ae  35383  4atlem0be  35384  4atlem3b  35387  4atlem9  35392  4atlem10a  35393  4atlem10  35395  4atlem11a  35396  4atlem12a  35399  4at2  35403  2lplnm2N  35410  lneq2at  35567  2llnma1b  35575  2llnma1  35576  2llnma3r  35577  2llnma2  35578  2llnma2rN  35579  cdlema1N  35580  paddasslem2  35610  paddasslem15  35623  paddasslem16  35624  pmodlem1  35635  pmodlem2  35636  pmod2iN  35638  hlmod1i  35645  atmod1i1m  35647  atmod2i1  35650  atmod2i2  35651  atmod3i1  35653  atmod3i2  35654  atmod4i1  35655  atmod4i2  35656  llnexchb2lem  35657  llnexch2N  35659  dalawlem3  35662  dalawlem4  35663  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem9  35668  dalawlem11  35670  dalawlem12  35671  dalawlem13  35672  dalawlem15  35674  osumcllem9N  35753  pl42lem1N  35768  4atexlems  35841  4atex2  35866  4atex2-0bOLDN  35868  trlval4  35978  cdlemc5  35985  cdlemc6  35986  cdlemd2  35989  cdlemd4  35991  cdlemd6  35993  cdleme00a  35999  cdleme0e  36007  cdleme3g  36024  cdleme3h  36025  cdleme3  36027  cdleme4  36028  cdleme4a  36029  cdleme5  36030  cdleme9  36043  cdleme16aN  36049  cdleme11c  36051  cdleme11e  36053  cdleme11g  36055  cdleme11h  36056  cdleme11j  36057  cdleme11k  36058  cdleme11l  36059  cdleme11  36060  cdleme12  36061  cdleme14  36063  cdleme15c  36066  cdleme16b  36069  cdleme16c  36070  cdleme16d  36071  cdleme16e  36072  cdleme16f  36073  cdleme0nex  36080  cdleme18a  36081  cdleme18c  36083  cdleme18d  36085  cdlemednpq  36089  cdlemednuN  36090  cdleme20zN  36091  cdleme20y  36092  cdleme19a  36093  cdleme19b  36094  cdleme19d  36096  cdleme19e  36097  cdleme20aN  36099  cdleme20bN  36100  cdleme20c  36101  cdleme20d  36102  cdleme20f  36104  cdleme20g  36105  cdleme20i  36107  cdleme20j  36108  cdleme20l1  36110  cdleme20l2  36111  cdleme20l  36112  cdleme20m  36113  cdleme21b  36116  cdleme21c  36117  cdleme21e  36121  cdleme21f  36122  cdleme22a  36130  cdleme22b  36131  cdleme22e  36134  cdleme22eALTN  36135  cdleme22f  36136  cdleme26eALTN  36151  cdleme26fALTN  36152  cdleme26f  36153  cdleme26f2ALTN  36154  cdleme26f2  36155  cdleme27N  36159  cdleme28a  36160  cdleme28b  36161  cdleme30a  36168  cdleme43fsv1snlem  36210  cdlemefs31fv1  36214  cdlemefs45eN  36221  cdleme32b  36232  cdleme32c  36233  cdleme32d  36234  cdleme35h  36246  cdleme36a  36250  cdleme36m  36251  cdleme37m  36252  cdleme40m  36257  cdleme40n  36258  cdleme41sn3aw  36264  cdleme41sn4aw  36265  cdleme41fva11  36267  cdleme42k  36274  cdleme43cN  36281  cdleme43dN  36282  cdleme46f2g1  36284  cdlemeg47rv2  36300  cdlemeg46sfg  36310  cdlemeg46fjgN  36311  cdlemeg46rjgN  36312  cdlemeg46fjv  36313  cdlemeg46frv  36315  cdlemeg46vrg  36317  cdlemeg46rgv  36318  cdlemeg46req  36319  cdlemeg46gfv  36320  cdlemg4a  36398  cdlemg4d  36403  cdlemg4e  36404  cdlemg4f  36405  cdlemg4g  36406  cdlemg4  36407  cdlemg6d  36411  cdlemg6e  36412  cdlemg8b  36418  cdlemg8c  36419  cdlemg9a  36422  cdlemg9b  36423  cdlemg10a  36430  cdlemg10  36431  cdlemg12a  36433  cdlemg12b  36434  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg17dN  36453  cdlemg17dALTN  36454  cdlemg17e  36455  cdlemg17f  36456  cdlemg17g  36457  cdlemg17h  36458  cdlemg17i  36459  cdlemg17pq  36462  cdlemg17iqN  36464  cdlemg17  36467  cdlemg18b  36469  cdlemg18c  36470  cdlemg19a  36473  cdlemg19  36474  cdlemg28a  36483  cdlemg27b  36486  cdlemg28b  36493  cdlemg28  36494  cdlemg33a  36496  cdlemg33b  36497  cdlemg33c  36498  cdlemg33d  36499  cdlemg33e  36500  cdlemg33  36501  cdlemg35  36503  cdlemg36  36504  cdlemg44a  36521  cdlemh  36607  cdlemi2  36609  cdlemj1  36611  tendocan  36614  cdlemk5a  36625  cdlemki  36631  cdlemkvcl  36632  cdlemk10  36633  cdlemksv2  36637  cdlemkole  36643  cdlemk14  36644  cdlemk15  36645  cdlemk16a  36646  cdlemk16  36647  cdlemk17  36648  cdlemk18  36658  cdlemk19  36659  cdlemkoatnle-2N  36665  cdlemk13-2N  36666  cdlemkole-2N  36667  cdlemk14-2N  36668  cdlemk15-2N  36669  cdlemk16-2N  36670  cdlemk17-2N  36671  cdlemk18-2N  36676  cdlemk19-2N  36677  cdlemk30  36684  cdlemk18-3N  36690  cdlemk23-3  36692  cdlemk25-3  36694  cdlemk27-3  36697  cdlemk37  36704  cdlemkfid1N  36711  cdlemkid1  36712  cdlemky  36716  cdlemk11ta  36719  cdlemk47  36739  cdlemk48  36740  cdlemk49  36741  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  cdlemk53a  36745  cdlemk54  36748  cdlemk39u1  36757  cdlemk19u1  36759  cdleml1N  36766  cdleml2N  36767  cdleml3N  36768  dia2dimlem6  36860  cdlemn2  36986  cdlemn2a  36987  cdlemn5pre  36991  cdlemn10  36997  cdlemn11c  37000  cdlemn11pre  37001  dihjustlem  37007  dihjust  37008  lclkrlem2y  37322  relexpmulnn  38503  lincreslvec3  42781  amgmwlem  43061
  Copyright terms: Public domain W3C validator