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

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

Proof of Theorem simp23
StepHypRef Expression
1 simp3 1168 . 2 ((𝜓𝜒𝜃) → 𝜃)
213ad2ant2 1164 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107
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 1109
This theorem is referenced by:  simpl23OLD  1340  simpr23OLD  1358  simp123  1406  simp223  1415  simp323  1424  omeulem1  7867  elfiun  8543  cofsmo  9344  modexp  13206  iscatd2  16607  funcoppc  16800  funcres  16821  catcisolem  17021  1stfcl  17103  2ndfcl  17104  prfcl  17109  evlfcl  17128  curf1cl  17134  curfcl  17138  hofcl  17165  pmtrprfv3  18137  mdetunilem3  20697  mdetunilem4  20698  mdetuni0  20704  mdetmul  20706  prdsxmetlem  22452  isosctrlem3  24841  isosctr  24842  f1otrg  26042  colinearalg  26081  ax5seglem6  26105  ax5seg  26109  axpasch  26112  axeuclid  26134  uhgr2edg  26378  clwwlkccat  27217  ogrpsub  30164  ogrpsublt  30169  rhmdvd  30268  bnj966  31462  bnj967  31463  mclspps  31929  cgrtr  32543  cgrtr3  32545  ofscom  32558  btwnxfr  32607  colinearxfr  32626  lineext  32627  brofs2  32628  brifs2  32629  fscgr  32631  linecgr  32632  btwnconn1lem1  32638  btwnconn1lem2  32639  btwnconn1lem3  32640  btwnconn1lem4  32641  btwnconn1lem5  32642  btwnconn1lem6  32643  btwnconn1lem7  32644  seglecgr12im  32661  seglecgr12  32662  segletr  32665  broutsideof3  32677  outsideofeq  32681  lineunray  32698  eqlkr  35055  omlmod1i2N  35216  cvrcmp2  35240  cvlexch2  35285  cvlexchb2  35287  cvlatexchb2  35291  cvlatexch1  35292  cvlatexch2  35293  cvlatexch3  35294  cvlsupr7  35304  cvlsupr8  35305  atnlej1  35335  atnlej2  35336  2llnneN  35365  cvratlem  35377  atcvrneN  35386  atcvrj1  35387  atlelt  35394  2atjm  35401  3noncolr2  35405  3noncolr1N  35406  hlatcon2  35408  3dimlem2  35415  3dim1  35423  3dim2  35424  1cvrat  35432  ps-1  35433  ps-2  35434  2atjlej  35435  hlatexch3N  35436  ps-2b  35438  3atlem1  35439  3atlem2  35440  3atlem6  35444  llnle  35474  2atm  35483  ps-2c  35484  lplni2  35493  lplnle  35496  lplnnle2at  35497  lplnri3N  35511  llncvrlpln2  35513  2atmat  35517  2llnjaN  35522  2llnm2N  35524  2llnm4  35526  2llnmeqat  35527  lvolnle3at  35538  4atlem0ae  35550  4atlem0be  35551  4atlem3b  35554  4atlem9  35559  4atlem10a  35560  4atlem10  35562  4atlem11a  35563  4atlem12a  35566  4at  35569  4at2  35570  lplncvrlvol2  35571  2lplnm2N  35577  2llnma1b  35742  2llnma1  35743  2llnma3r  35744  2llnma2  35745  2llnma2rN  35746  cdlema1N  35747  cdlema2N  35748  paddasslem2  35777  paddasslem15  35790  paddasslem16  35791  pmodlem1  35802  pmod2iN  35805  hlmod1i  35812  atmod2i1  35817  atmod2i2  35818  atmod3i1  35820  atmod3i2  35821  atmod4i1  35822  atmod4i2  35823  llnexchb2  35825  dalawlem3  35829  dalawlem4  35830  dalawlem5  35831  dalawlem6  35832  dalawlem7  35833  dalawlem8  35834  dalawlem9  35835  dalawlem11  35837  dalawlem13  35839  dalawlem15  35841  osumcllem7N  35918  osumcllem9N  35920  osumcllem11N  35922  pl42lem1N  35935  4atex  36032  4atex2-0aOLDN  36034  4atex2-0bOLDN  36035  4atex2-0cOLDN  36036  trlval4  36144  cdlemc5  36151  cdlemd5  36158  cdlemd6  36159  cdleme00a  36165  cdleme3g  36190  cdleme3h  36191  cdleme3  36193  cdleme4  36194  cdleme4a  36195  cdleme16aN  36215  cdleme11c  36217  cdleme11g  36221  cdleme11h  36222  cdleme12  36227  cdleme0nex  36246  cdleme18a  36247  cdleme18b  36248  cdleme18c  36249  cdleme18d  36251  cdleme20zN  36257  cdleme20y  36258  cdleme19a  36259  cdleme19b  36260  cdleme19d  36262  cdleme19e  36263  cdleme20aN  36265  cdleme20c  36267  cdleme20d  36268  cdleme20i  36273  cdleme20j  36274  cdleme20l1  36276  cdleme20l2  36277  cdleme20m  36279  cdleme21b  36282  cdleme21c  36283  cdleme21j  36292  cdleme22aa  36295  cdleme22a  36296  cdleme22eALTN  36301  cdleme26e  36315  cdleme26fALTN  36318  cdleme26f  36319  cdleme26f2ALTN  36320  cdleme26f2  36321  cdleme27N  36325  cdleme28a  36326  cdleme28b  36327  cdleme30a  36334  cdlemefs45eN  36387  cdleme32c  36399  cdleme32e  36401  cdleme35h  36412  cdleme36a  36416  cdleme36m  36417  cdleme37m  36418  cdleme41sn3aw  36430  cdleme41sn4aw  36431  cdleme41fva11  36433  cdleme42k  36440  cdleme43cN  36447  cdleme43dN  36448  cdleme46f2g1  36450  cdlemeg47rv2  36466  cdlemeg46sfg  36476  cdlemeg46fjgN  36477  cdlemeg46rjgN  36478  cdlemeg46fjv  36479  cdlemeg46frv  36481  cdlemeg46vrg  36483  cdlemeg46rgv  36484  cdlemeg46req  36485  cdlemeg46gfv  36486  cdleme50trn2a  36506  cdlemg2fv2  36556  cdlemg4a  36564  cdlemg4e  36570  cdlemg4f  36571  cdlemg8b  36584  cdlemg8c  36585  cdlemg9a  36588  cdlemg9b  36589  cdlemg9  36590  cdlemg10a  36596  cdlemg12a  36599  cdlemg12b  36600  cdlemg12c  36601  cdlemg12  36606  cdlemg17dN  36619  cdlemg17dALTN  36620  cdlemg17e  36621  cdlemg17i  36625  cdlemg17ir  36626  cdlemg17pq  36628  cdlemg17bq  36629  cdlemg17iqN  36630  cdlemg17  36633  cdlemg18b  36635  cdlemg18c  36636  cdlemg18d  36637  cdlemg18  36638  cdlemg19  36640  cdlemg21  36642  cdlemg28a  36649  cdlemg31b0a  36651  cdlemg33b0  36657  cdlemg35  36669  cdlemg44a  36687  cdlemh  36773  cdlemi2  36775  cdlemj1  36777  cdlemk5a  36791  cdlemk5  36792  cdlemki  36797  cdlemkvcl  36798  cdlemk10  36799  cdlemksv2  36803  cdlemk7  36804  cdlemk11  36805  cdlemk12  36806  cdlemk15  36811  cdlemk16a  36812  cdlemk16  36813  cdlemk5u  36817  cdlemk6u  36818  cdlemk18  36824  cdlemk19  36825  cdlemk7u  36826  cdlemk11u  36827  cdlemk12u  36828  cdlemk21N  36829  cdlemk20  36830  cdlemkoatnle-2N  36831  cdlemk13-2N  36832  cdlemkole-2N  36833  cdlemk14-2N  36834  cdlemk15-2N  36835  cdlemk16-2N  36836  cdlemk17-2N  36837  cdlemk18-2N  36842  cdlemk19-2N  36843  cdlemk22  36849  cdlemk30  36850  cdlemk28-3  36864  cdlemk33N  36865  cdlemkfid1N  36877  cdlemkid1  36878  cdlemky  36882  cdlemk11ta  36885  cdlemk35s-id  36894  cdlemk39s-id  36896  cdlemk47  36905  cdlemk48  36906  cdlemk49  36907  cdlemk50  36908  cdlemk51  36909  cdlemk52  36910  cdlemk53a  36911  cdlemk53b  36912  cdlemk53  36913  cdlemk54  36914  cdlemk55a  36915  cdlemkyyN  36918  cdlemk43N  36919  cdlemk55u1  36921  cdlemk55u  36922  cdlemk39u1  36923  cdlemk19u1  36925  cdleml1N  36932  cdleml2N  36933  cdleml3N  36934  dia2dimlem6  37025  cdlemn2  37151  cdlemn2a  37152  cdlemn5pre  37156  cdlemn11pre  37166  dihjustlem  37172  dihjust  37173  dihmeetlem15N  37277  lclkrlem2y  37487  relexpxpnnidm  38670
  Copyright terms: Public domain W3C validator