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

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

Proof of Theorem simp21
StepHypRef Expression
1 simp1 1081 . 2 ((𝜓𝜒𝜃) → 𝜓)
213ad2ant2 1103 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 1056
This theorem is referenced by:  simpl21  1159  simpr21  1168  simp121  1213  simp221  1222  simp321  1231  omeulem1  7707  cofsmo  9129  axdc4lem  9315  0catg  16395  funcoppc  16582  funcres  16603  catcisolem  16803  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  curfcl  16919  hofcl  16946  mulgdirlem  17619  mdetunilem4  20469  mdetuni0  20475  mdetmul  20477  prdsxmetlem  22220  isosctrlem3  24595  isosctr  24596  amgmlem  24761  f1otrg  25796  colinearalg  25835  ax5seglem6  25859  ax5seg  25863  axpasch  25866  axeuclidlem  25887  axeuclid  25888  uhgr2edg  26145  ogrpsub  29845  ogrpaddlt  29846  ogrpsublt  29850  rhmdvd  29949  bnj1128  31184  mclspps  31607  nosupbnd2lem1  31986  cgrtr  32224  cgrtr3  32226  ofscom  32239  segconeq  32242  ifscgr  32276  btwnxfr  32288  colinearxfr  32307  lineext  32308  brofs2  32309  brifs2  32310  fscgr  32312  linecgr  32313  btwnconn1lem1  32319  btwnconn1lem2  32320  btwnconn1lem3  32321  btwnconn1lem4  32322  btwnconn1lem5  32323  btwnconn1lem6  32324  btwnconn1lem7  32325  seglecgr12im  32342  seglecgr12  32343  segletr  32346  broutsideof3  32358  outsideofeq  32362  lineunray  32379  lineelsb2  32380  linecom  32382  lshpkrlem5  34719  omlmod1i2N  34865  cvrnbtwn3  34881  cvrcmp  34888  cvrcmp2  34889  cvlexch2  34934  cvlexchb2  34936  cvlatexchb2  34940  cvlatexch2  34942  cvlatexch3  34943  cvlsupr7  34953  atnlej1  34983  atnlej2  34984  2llnneN  35013  cvratlem  35025  atcvrneN  35034  atcvrj1  35035  atlelt  35042  2atjm  35049  3noncolr2  35053  3noncolr1N  35054  3dimlem2  35063  3dim1  35071  3dim2  35072  1cvrat  35080  ps-1  35081  ps-2  35082  2atjlej  35083  hlatexch3N  35084  ps-2b  35086  3atlem1  35087  3atlem2  35088  3atlem5  35091  3atlem6  35092  llnle  35122  2atm  35131  ps-2c  35132  lplni2  35141  lplnle  35144  lplnnle2at  35145  lplnri3N  35159  llncvrlpln2  35161  2atmat  35165  2llnm2N  35172  2llnm4  35174  2llnmeqat  35175  lvolnle3at  35186  4atlem0ae  35198  4atlem0be  35199  4atlem3b  35202  4atlem9  35207  4atlem10a  35208  4atlem10  35210  4atlem11a  35211  4atlem12a  35214  4at2  35218  2lplnm2N  35225  lneq2at  35382  2llnma1b  35390  2llnma1  35391  2llnma3r  35392  2llnma2  35393  2llnma2rN  35394  cdlema1N  35395  paddasslem2  35425  paddasslem15  35438  paddasslem16  35439  pmodlem1  35450  pmodlem2  35451  pmod2iN  35453  hlmod1i  35460  atmod1i1m  35462  atmod2i1  35465  atmod2i2  35466  atmod3i1  35468  atmod3i2  35469  atmod4i1  35470  atmod4i2  35471  llnexchb2lem  35472  llnexch2N  35474  dalawlem3  35477  dalawlem4  35478  dalawlem5  35479  dalawlem6  35480  dalawlem7  35481  dalawlem8  35482  dalawlem9  35483  dalawlem11  35485  dalawlem12  35486  dalawlem13  35487  dalawlem15  35489  osumcllem9N  35568  pl42lem1N  35583  4atexlems  35656  4atex2  35681  4atex2-0bOLDN  35683  trlval4  35793  cdlemc5  35800  cdlemc6  35801  cdlemd2  35804  cdlemd4  35806  cdlemd6  35808  cdleme00a  35814  cdleme0e  35822  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme4  35843  cdleme4a  35844  cdleme5  35845  cdleme9  35858  cdleme16aN  35864  cdleme11c  35866  cdleme11e  35868  cdleme11g  35870  cdleme11h  35871  cdleme11j  35872  cdleme11k  35873  cdleme11l  35874  cdleme11  35875  cdleme12  35876  cdleme14  35878  cdleme15c  35881  cdleme16b  35884  cdleme16c  35885  cdleme16d  35886  cdleme16e  35887  cdleme16f  35888  cdleme0nex  35895  cdleme18a  35896  cdleme18c  35898  cdleme18d  35900  cdlemednpq  35904  cdlemednuN  35905  cdleme20zN  35906  cdleme20y  35907  cdleme19a  35908  cdleme19b  35909  cdleme19d  35911  cdleme19e  35912  cdleme20aN  35914  cdleme20bN  35915  cdleme20c  35916  cdleme20d  35917  cdleme20f  35919  cdleme20g  35920  cdleme20i  35922  cdleme20j  35923  cdleme20l1  35925  cdleme20l2  35926  cdleme20l  35927  cdleme20m  35928  cdleme21b  35931  cdleme21c  35932  cdleme21e  35936  cdleme21f  35937  cdleme22a  35945  cdleme22b  35946  cdleme22e  35949  cdleme22eALTN  35950  cdleme22f  35951  cdleme26eALTN  35966  cdleme26fALTN  35967  cdleme26f  35968  cdleme26f2ALTN  35969  cdleme26f2  35970  cdleme27N  35974  cdleme28a  35975  cdleme28b  35976  cdleme30a  35983  cdleme43fsv1snlem  36025  cdlemefs31fv1  36029  cdlemefs45eN  36036  cdleme32b  36047  cdleme32c  36048  cdleme32d  36049  cdleme35h  36061  cdleme36a  36065  cdleme36m  36066  cdleme37m  36067  cdleme40m  36072  cdleme40n  36073  cdleme41sn3aw  36079  cdleme41sn4aw  36080  cdleme41fva11  36082  cdleme42k  36089  cdleme43cN  36096  cdleme43dN  36097  cdleme46f2g1  36099  cdlemeg47rv2  36115  cdlemeg46sfg  36125  cdlemeg46fjgN  36126  cdlemeg46rjgN  36127  cdlemeg46fjv  36128  cdlemeg46frv  36130  cdlemeg46vrg  36132  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemeg46gfv  36135  cdlemg4a  36213  cdlemg4d  36218  cdlemg4e  36219  cdlemg4f  36220  cdlemg4g  36221  cdlemg4  36222  cdlemg6d  36226  cdlemg6e  36227  cdlemg8b  36233  cdlemg8c  36234  cdlemg9a  36237  cdlemg9b  36238  cdlemg10a  36245  cdlemg10  36246  cdlemg12a  36248  cdlemg12b  36249  cdlemg12f  36253  cdlemg12g  36254  cdlemg12  36255  cdlemg17dN  36268  cdlemg17dALTN  36269  cdlemg17e  36270  cdlemg17f  36271  cdlemg17g  36272  cdlemg17h  36273  cdlemg17i  36274  cdlemg17pq  36277  cdlemg17iqN  36279  cdlemg17  36282  cdlemg18b  36284  cdlemg18c  36285  cdlemg19a  36288  cdlemg19  36289  cdlemg28a  36298  cdlemg27b  36301  cdlemg28b  36308  cdlemg28  36309  cdlemg33a  36311  cdlemg33b  36312  cdlemg33c  36313  cdlemg33d  36314  cdlemg33e  36315  cdlemg33  36316  cdlemg35  36318  cdlemg36  36319  cdlemg44a  36336  cdlemh  36422  cdlemi2  36424  cdlemj1  36426  tendocan  36429  cdlemk5a  36440  cdlemki  36446  cdlemkvcl  36447  cdlemk10  36448  cdlemksv2  36452  cdlemkole  36458  cdlemk14  36459  cdlemk15  36460  cdlemk16a  36461  cdlemk16  36462  cdlemk17  36463  cdlemk18  36473  cdlemk19  36474  cdlemkoatnle-2N  36480  cdlemk13-2N  36481  cdlemkole-2N  36482  cdlemk14-2N  36483  cdlemk15-2N  36484  cdlemk16-2N  36485  cdlemk17-2N  36486  cdlemk18-2N  36491  cdlemk19-2N  36492  cdlemk30  36499  cdlemk18-3N  36505  cdlemk23-3  36507  cdlemk25-3  36509  cdlemk27-3  36512  cdlemk37  36519  cdlemkfid1N  36526  cdlemkid1  36527  cdlemky  36531  cdlemk11ta  36534  cdlemk47  36554  cdlemk48  36555  cdlemk49  36556  cdlemk50  36557  cdlemk51  36558  cdlemk52  36559  cdlemk53a  36560  cdlemk54  36563  cdlemk39u1  36572  cdlemk19u1  36574  cdleml1N  36581  cdleml2N  36582  cdleml3N  36583  dia2dimlem6  36675  cdlemn2  36801  cdlemn2a  36802  cdlemn5pre  36806  cdlemn10  36812  cdlemn11c  36815  cdlemn11pre  36816  dihjustlem  36822  dihjust  36823  lclkrlem2y  37137  relexpmulnn  38318  lincreslvec3  42596  amgmwlem  42876
  Copyright terms: Public domain W3C validator