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

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

Proof of Theorem simp22
StepHypRef Expression
1 simp2 1160 . 2 ((𝜓𝜒𝜃) → 𝜒)
213ad2ant2 1157 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simpl22OLD  1331  simpr22OLD  1349  simp122  1398  simp222  1407  simp322  1416  elfiun  8585  cofsmo  9386  modexp  13242  funcoppc  16759  funcres  16780  catcisolem  16980  1stfcl  17062  2ndfcl  17063  prfcl  17068  evlfcl  17087  curf1cl  17093  curfcl  17097  hofcl  17124  mulgdirlem  17795  pmtrprfv3  18095  mdetunilem4  20653  mdetuni0  20659  mdetmul  20661  prdsxmetlem  22407  isosctrlem3  24787  isosctr  24788  amgmlem  24953  f1otrg  25988  colinearalg  26027  ax5seglem6  26051  ax5seg  26055  axpasch  26058  axeuclidlem  26079  axeuclid  26080  ogrpsub  30065  ogrpaddlt  30066  ogrpsublt  30070  rhmdvd  30169  bnj966  31359  mclspps  31826  cgrtr  32442  cgrtr3  32444  ofscom  32457  cgrextend  32458  btwnxfr  32506  colinearxfr  32525  lineext  32526  fscgr  32530  linecgr  32531  btwnconn1lem1  32537  btwnconn1lem2  32538  btwnconn1lem3  32539  btwnconn1lem4  32540  btwnconn1lem5  32541  btwnconn1lem6  32542  btwnconn1lem7  32543  seglecgr12im  32560  seglecgr12  32561  segletr  32564  broutsideof3  32576  outsideofeq  32580  lineunray  32597  linecom  32600  eqlkr  34898  lshpkrlem5  34913  omlmod1i2N  35059  cvrnbtwn3  35075  cvrcmp2  35083  cvlexch2  35128  cvlexchb2  35130  cvlatexchb2  35134  cvlatexch1  35135  cvlatexch2  35136  cvlatexch3  35137  cvlsupr7  35147  cvlsupr8  35148  atnlej1  35178  atnlej2  35179  2llnneN  35208  cvratlem  35220  atcvrneN  35229  atlelt  35237  2atjm  35244  3noncolr2  35248  3noncolr1N  35249  hlatcon2  35251  3dimlem2  35258  3dim1  35266  3dim2  35267  1cvrat  35275  ps-1  35276  ps-2  35277  2atjlej  35278  hlatexch3N  35279  ps-2b  35281  3atlem1  35282  3atlem5  35286  3atlem6  35287  2atm  35326  ps-2c  35327  lplni2  35336  lplnri3N  35354  llncvrlpln2  35356  2atmat  35360  2llnm2N  35367  2llnm3N  35368  2llnm4  35369  2llnmeqat  35370  lvolnle3at  35381  4atlem0ae  35393  4atlem0be  35394  4atlem3b  35397  4atlem9  35402  4atlem10a  35403  4atlem10  35405  4atlem11a  35406  4atlem12a  35409  4at2  35413  2lplnm2N  35420  lneq2at  35577  2llnma1b  35585  2llnma1  35586  2llnma3r  35587  2llnma2  35588  2llnma2rN  35589  cdlema1N  35590  paddasslem2  35620  paddasslem16  35634  pmodlem1  35645  pmod2iN  35648  hlmod1i  35655  atmod2i1  35660  atmod2i2  35661  atmod3i1  35663  atmod3i2  35664  atmod4i1  35665  atmod4i2  35666  llnexchb2lem  35667  llnexch2N  35669  dalawlem3  35672  dalawlem4  35673  dalawlem5  35674  dalawlem6  35675  dalawlem7  35676  dalawlem8  35677  dalawlem9  35678  dalawlem11  35680  dalawlem12  35681  dalawlem13  35682  dalawlem15  35684  osumcllem7N  35761  osumcllem9N  35763  pl42lem1N  35778  4atexlemswapqr  35862  4atex2  35876  4atex2-0bOLDN  35878  trlval4  35987  cdlemc5  35994  cdlemc6  35995  cdlemd2  35998  cdlemd4  36000  cdlemd6  36002  cdleme00a  36008  cdleme0e  36016  cdleme4  36037  cdleme4a  36038  cdleme5  36039  cdleme9  36052  cdleme16aN  36058  cdleme11c  36060  cdleme11dN  36061  cdleme11e  36062  cdleme11g  36064  cdleme11h  36065  cdleme11j  36066  cdleme11k  36067  cdleme11l  36068  cdleme11  36069  cdleme12  36070  cdleme13  36071  cdleme14  36072  cdleme15a  36073  cdleme15c  36075  cdleme16b  36078  cdleme16c  36079  cdleme16d  36080  cdleme16e  36081  cdleme16f  36082  cdleme17d1  36088  cdleme0nex  36089  cdleme18a  36090  cdleme18b  36091  cdleme18c  36092  cdleme18d  36094  cdlemednpq  36098  cdlemednuN  36099  cdleme20zN  36100  cdleme20y  36101  cdleme19a  36102  cdleme19b  36103  cdleme19d  36105  cdleme19e  36106  cdleme20aN  36108  cdleme20d  36111  cdleme20f  36113  cdleme20g  36114  cdleme20i  36116  cdleme20j  36117  cdleme20l1  36119  cdleme20l2  36120  cdleme20l  36121  cdleme20m  36122  cdleme21b  36125  cdleme21c  36126  cdleme21e  36130  cdleme21j  36135  cdleme22aa  36138  cdleme22a  36139  cdleme22b  36140  cdleme22cN  36141  cdleme22d  36142  cdleme22e  36143  cdleme22eALTN  36144  cdleme22f  36145  cdleme26fALTN  36161  cdleme26f  36162  cdleme26f2ALTN  36163  cdleme26f2  36164  cdleme27N  36168  cdleme28a  36169  cdleme28b  36170  cdleme30a  36177  cdlemefs31fv1  36223  cdleme32b  36241  cdleme32c  36242  cdleme32e  36244  cdleme35h  36255  cdleme36a  36259  cdleme36m  36260  cdleme41sn3aw  36273  cdleme41sn4aw  36274  cdleme41fva11  36276  cdleme42k  36283  cdleme43cN  36290  cdleme46f2g1  36293  cdlemeg46fjgN  36320  cdlemeg46fjv  36322  cdlemeg46frv  36324  cdlemeg46rgv  36327  cdlemeg46req  36328  cdlemeg46gfv  36329  cdleme50trn2a  36349  cdlemg4a  36407  cdlemg4d  36412  cdlemg4e  36413  cdlemg4f  36414  cdlemg8c  36428  cdlemg9a  36431  cdlemg9b  36432  cdlemg10a  36439  cdlemg10  36440  cdlemg12b  36443  cdlemg12f  36447  cdlemg12g  36448  cdlemg12  36449  cdlemg17dN  36462  cdlemg17dALTN  36463  cdlemg17e  36464  cdlemg17f  36465  cdlemg17g  36466  cdlemg17i  36468  cdlemg17ir  36469  cdlemg17pq  36471  cdlemg17bq  36472  cdlemg17iqN  36473  cdlemg17  36476  cdlemg18b  36478  cdlemg18c  36479  cdlemg18d  36480  cdlemg18  36481  cdlemg19  36483  cdlemg21  36485  cdlemg28a  36492  cdlemg31b0a  36494  cdlemg27b  36495  cdlemg33b0  36500  cdlemg28b  36502  cdlemg28  36503  cdlemg35  36512  cdlemg36  36513  cdlemg44a  36530  cdlemh  36616  cdlemi2  36618  cdlemj1  36620  tendocan  36623  cdlemk5a  36634  cdlemk5  36635  cdlemki  36640  cdlemkvcl  36641  cdlemk10  36642  cdlemksv2  36646  cdlemk7  36647  cdlemk11  36648  cdlemk12  36649  cdlemkoatnle  36650  cdlemk15  36654  cdlemk16a  36655  cdlemk16  36656  cdlemk1u  36658  cdlemk5u  36660  cdlemk6u  36661  cdlemk18  36667  cdlemk19  36668  cdlemk7u  36669  cdlemk11u  36670  cdlemk12u  36671  cdlemk21N  36672  cdlemk20  36673  cdlemkoatnle-2N  36674  cdlemk13-2N  36675  cdlemkole-2N  36676  cdlemk14-2N  36677  cdlemk15-2N  36678  cdlemk16-2N  36679  cdlemk17-2N  36680  cdlemk18-2N  36685  cdlemk19-2N  36686  cdlemk22  36692  cdlemk30  36693  cdlemkuel-3  36697  cdlemkuv2-3N  36698  cdlemk18-3N  36699  cdlemkfid1N  36720  cdlemkid1  36721  cdlemkfid3N  36724  cdlemky  36725  cdlemk11ta  36728  cdlemk47  36748  cdlemk48  36749  cdlemk49  36750  cdlemk50  36751  cdlemk51  36752  cdlemk52  36753  cdlemk53a  36754  cdlemk53  36756  cdlemk54  36757  cdlemk55a  36758  cdlemkyyN  36761  cdlemk43N  36762  cdlemk55u1  36764  cdlemk55u  36765  cdlemk39u1  36766  cdlemk19u1  36768  cdleml1N  36775  cdleml2N  36776  cdleml3N  36777  dia2dimlem6  36868  cdlemn2  36994  cdlemn2a  36995  cdlemn5pre  36999  cdlemn11a  37006  dihjustlem  37015  dihjust  37016  dihmeetlem15N  37120  lclkrlem2y  37330  relexpmulnn  38519  amgmwlem  43137
  Copyright terms: Public domain W3C validator