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

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

Proof of Theorem simp22
StepHypRef Expression
1 simp2 1134 . 2 ((𝜓𝜒𝜃) → 𝜒)
213ad2ant2 1131 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simp122  1303  simp222  1312  simp322  1321  elfiun  8882  cofsmo  9680  modexp  13595  funcoppc  17136  funcres  17157  catcisolem  17357  1stfcl  17438  2ndfcl  17439  prfcl  17444  evlfcl  17463  curf1cl  17469  curfcl  17473  hofcl  17500  mulgdirlem  18249  pmtrprfv3  18573  mdetunilem4  21218  mdetuni0  21224  mdetmul  21226  prdsxmetlem  22973  isosctrlem3  25404  isosctr  25405  amgmlem  25573  f1otrg  26663  colinearalg  26702  ax5seglem6  26726  ax5seg  26730  axpasch  26733  axeuclidlem  26754  axeuclid  26755  ogrpsub  30748  ogrpaddlt  30749  ogrpsublt  30753  rhmdvd  30926  bnj966  32290  mclspps  32905  cgrtr  33527  cgrtr3  33529  ofscom  33542  cgrextend  33543  btwnxfr  33591  colinearxfr  33610  lineext  33611  fscgr  33615  linecgr  33616  btwnconn1lem1  33622  btwnconn1lem2  33623  btwnconn1lem3  33624  btwnconn1lem4  33625  btwnconn1lem5  33626  btwnconn1lem6  33627  btwnconn1lem7  33628  seglecgr12im  33645  seglecgr12  33646  segletr  33649  broutsideof3  33661  outsideofeq  33665  lineunray  33682  linecom  33685  eqlkr  36354  lshpkrlem5  36369  omlmod1i2N  36515  cvrnbtwn3  36531  cvrcmp2  36539  cvlexch2  36584  cvlexchb2  36586  cvlatexchb2  36590  cvlatexch1  36591  cvlatexch2  36592  cvlatexch3  36593  cvlsupr7  36603  cvlsupr8  36604  atnlej1  36634  atnlej2  36635  2llnneN  36664  cvratlem  36676  atcvrneN  36685  atlelt  36693  2atjm  36700  3noncolr2  36704  3noncolr1N  36705  hlatcon2  36707  3dimlem2  36714  3dim1  36722  3dim2  36723  1cvrat  36731  ps-1  36732  ps-2  36733  2atjlej  36734  hlatexch3N  36735  ps-2b  36737  3atlem1  36738  3atlem5  36742  3atlem6  36743  2atm  36782  ps-2c  36783  lplni2  36792  lplnri3N  36810  llncvrlpln2  36812  2atmat  36816  2llnm2N  36823  2llnm3N  36824  2llnm4  36825  2llnmeqat  36826  lvolnle3at  36837  4atlem0ae  36849  4atlem0be  36850  4atlem3b  36853  4atlem9  36858  4atlem10a  36859  4atlem10  36861  4atlem11a  36862  4atlem12a  36865  4at2  36869  2lplnm2N  36876  lneq2at  37033  2llnma1b  37041  2llnma1  37042  2llnma3r  37043  2llnma2  37044  2llnma2rN  37045  cdlema1N  37046  paddasslem2  37076  paddasslem16  37090  pmodlem1  37101  pmod2iN  37104  hlmod1i  37111  atmod2i1  37116  atmod2i2  37117  atmod3i1  37119  atmod3i2  37120  atmod4i1  37121  atmod4i2  37122  llnexchb2lem  37123  llnexch2N  37125  dalawlem3  37128  dalawlem4  37129  dalawlem5  37130  dalawlem6  37131  dalawlem7  37132  dalawlem8  37133  dalawlem9  37134  dalawlem11  37136  dalawlem12  37137  dalawlem13  37138  dalawlem15  37140  osumcllem7N  37217  osumcllem9N  37219  pl42lem1N  37234  4atexlemswapqr  37318  4atex2  37332  4atex2-0bOLDN  37334  trlval4  37443  cdlemc5  37450  cdlemc6  37451  cdlemd2  37454  cdlemd4  37456  cdlemd6  37458  cdleme00a  37464  cdleme0e  37472  cdleme4  37493  cdleme4a  37494  cdleme5  37495  cdleme9  37508  cdleme16aN  37514  cdleme11c  37516  cdleme11dN  37517  cdleme11e  37518  cdleme11g  37520  cdleme11h  37521  cdleme11j  37522  cdleme11k  37523  cdleme11l  37524  cdleme11  37525  cdleme12  37526  cdleme13  37527  cdleme14  37528  cdleme15a  37529  cdleme15c  37531  cdleme16b  37534  cdleme16c  37535  cdleme16d  37536  cdleme16e  37537  cdleme16f  37538  cdleme17d1  37544  cdleme0nex  37545  cdleme18a  37546  cdleme18b  37547  cdleme18c  37548  cdleme18d  37550  cdlemednpq  37554  cdlemednuN  37555  cdleme20zN  37556  cdleme20y  37557  cdleme19a  37558  cdleme19b  37559  cdleme19d  37561  cdleme19e  37562  cdleme20aN  37564  cdleme20d  37567  cdleme20f  37569  cdleme20g  37570  cdleme20i  37572  cdleme20j  37573  cdleme20l1  37575  cdleme20l2  37576  cdleme20l  37577  cdleme20m  37578  cdleme21b  37581  cdleme21c  37582  cdleme21e  37586  cdleme21j  37591  cdleme22aa  37594  cdleme22a  37595  cdleme22b  37596  cdleme22cN  37597  cdleme22d  37598  cdleme22e  37599  cdleme22eALTN  37600  cdleme22f  37601  cdleme26fALTN  37617  cdleme26f  37618  cdleme26f2ALTN  37619  cdleme26f2  37620  cdleme27N  37624  cdleme28a  37625  cdleme28b  37626  cdleme30a  37633  cdlemefs31fv1  37679  cdleme32b  37697  cdleme32c  37698  cdleme32e  37700  cdleme35h  37711  cdleme36a  37715  cdleme36m  37716  cdleme41sn3aw  37729  cdleme41sn4aw  37730  cdleme41fva11  37732  cdleme42k  37739  cdleme43cN  37746  cdleme46f2g1  37749  cdlemeg46fjgN  37776  cdlemeg46fjv  37778  cdlemeg46frv  37780  cdlemeg46rgv  37783  cdlemeg46req  37784  cdlemeg46gfv  37785  cdleme50trn2a  37805  cdlemg4a  37863  cdlemg4d  37868  cdlemg4e  37869  cdlemg4f  37870  cdlemg8c  37884  cdlemg9a  37887  cdlemg9b  37888  cdlemg10a  37895  cdlemg10  37896  cdlemg12b  37899  cdlemg12f  37903  cdlemg12g  37904  cdlemg12  37905  cdlemg17dN  37918  cdlemg17dALTN  37919  cdlemg17e  37920  cdlemg17f  37921  cdlemg17g  37922  cdlemg17i  37924  cdlemg17ir  37925  cdlemg17pq  37927  cdlemg17bq  37928  cdlemg17iqN  37929  cdlemg17  37932  cdlemg18b  37934  cdlemg18c  37935  cdlemg18d  37936  cdlemg18  37937  cdlemg19  37939  cdlemg21  37941  cdlemg28a  37948  cdlemg31b0a  37950  cdlemg27b  37951  cdlemg33b0  37956  cdlemg28b  37958  cdlemg28  37959  cdlemg35  37968  cdlemg36  37969  cdlemg44a  37986  cdlemh  38072  cdlemi2  38074  cdlemj1  38076  tendocan  38079  cdlemk5a  38090  cdlemk5  38091  cdlemki  38096  cdlemkvcl  38097  cdlemk10  38098  cdlemksv2  38102  cdlemk7  38103  cdlemk11  38104  cdlemk12  38105  cdlemkoatnle  38106  cdlemk15  38110  cdlemk16a  38111  cdlemk16  38112  cdlemk1u  38114  cdlemk5u  38116  cdlemk6u  38117  cdlemk18  38123  cdlemk19  38124  cdlemk7u  38125  cdlemk11u  38126  cdlemk12u  38127  cdlemk21N  38128  cdlemk20  38129  cdlemkoatnle-2N  38130  cdlemk13-2N  38131  cdlemkole-2N  38132  cdlemk14-2N  38133  cdlemk15-2N  38134  cdlemk16-2N  38135  cdlemk17-2N  38136  cdlemk18-2N  38141  cdlemk19-2N  38142  cdlemk22  38148  cdlemk30  38149  cdlemkuel-3  38153  cdlemkuv2-3N  38154  cdlemk18-3N  38155  cdlemkfid1N  38176  cdlemkid1  38177  cdlemkfid3N  38180  cdlemky  38181  cdlemk11ta  38184  cdlemk47  38204  cdlemk48  38205  cdlemk49  38206  cdlemk50  38207  cdlemk51  38208  cdlemk52  38209  cdlemk53a  38210  cdlemk53  38212  cdlemk54  38213  cdlemk55a  38214  cdlemkyyN  38217  cdlemk43N  38218  cdlemk55u1  38220  cdlemk55u  38221  cdlemk39u1  38222  cdlemk19u1  38224  cdleml1N  38231  cdleml2N  38232  cdleml3N  38233  dia2dimlem6  38324  cdlemn2  38450  cdlemn2a  38451  cdlemn5pre  38455  cdlemn11a  38462  dihjustlem  38471  dihjust  38472  dihmeetlem15N  38576  lclkrlem2y  38786  relexpmulnn  40341  amgmwlem  45270
  Copyright terms: Public domain W3C validator