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

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

Proof of Theorem simp23
StepHypRef Expression
1 simp3 1061 . 2 ((𝜓𝜒𝜃) → 𝜃)
213ad2ant2 1081 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  simpl23  1139  simpr23  1148  simp123  1193  simp223  1202  simp323  1211  funtpgOLD  5901  omeulem1  7607  elfiun  8280  cofsmo  9035  modexp  12939  iscatd2  16263  funcoppc  16456  funcres  16477  catcisolem  16677  1stfcl  16758  2ndfcl  16759  prfcl  16764  evlfcl  16783  curf1cl  16789  curfcl  16793  hofcl  16820  pmtrprfv3  17795  mdetunilem3  20339  mdetunilem4  20340  mdetuni0  20346  mdetmul  20348  prdsxmetlem  22083  isosctrlem3  24450  isosctr  24451  f1otrg  25651  colinearalg  25690  ax5seglem6  25714  ax5seg  25718  axpasch  25721  axeuclid  25743  uhgr2edg  25993  ogrpsub  29502  ogrpsublt  29507  rhmdvd  29606  bnj966  30722  bnj967  30723  mclspps  31189  cgrtr  31741  cgrtr3  31743  ofscom  31756  btwnxfr  31805  colinearxfr  31824  lineext  31825  brofs2  31826  brifs2  31827  fscgr  31829  linecgr  31830  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem3  31838  btwnconn1lem4  31839  btwnconn1lem5  31840  btwnconn1lem6  31841  btwnconn1lem7  31842  seglecgr12im  31859  seglecgr12  31860  segletr  31863  broutsideof3  31875  outsideofeq  31879  lineunray  31896  eqlkr  33866  omlmod1i2N  34027  cvrcmp2  34051  cvlexch2  34096  cvlexchb2  34098  cvlatexchb2  34102  cvlatexch1  34103  cvlatexch2  34104  cvlatexch3  34105  cvlsupr7  34115  cvlsupr8  34116  atnlej1  34145  atnlej2  34146  2llnneN  34175  cvratlem  34187  atcvrneN  34196  atcvrj1  34197  atlelt  34204  2atjm  34211  3noncolr2  34215  3noncolr1N  34216  hlatcon2  34218  3dimlem2  34225  3dim1  34233  3dim2  34234  1cvrat  34242  ps-1  34243  ps-2  34244  2atjlej  34245  hlatexch3N  34246  ps-2b  34248  3atlem1  34249  3atlem2  34250  3atlem6  34254  llnle  34284  2atm  34293  ps-2c  34294  lplni2  34303  lplnle  34306  lplnnle2at  34307  lplnri3N  34321  llncvrlpln2  34323  2atmat  34327  2llnjaN  34332  2llnm2N  34334  2llnm4  34336  2llnmeqat  34337  lvolnle3at  34348  4atlem0ae  34360  4atlem0be  34361  4atlem3b  34364  4atlem9  34369  4atlem10a  34370  4atlem10  34372  4atlem11a  34373  4atlem12a  34376  4at  34379  4at2  34380  lplncvrlvol2  34381  2lplnm2N  34387  2llnma1b  34552  2llnma1  34553  2llnma3r  34554  2llnma2  34555  2llnma2rN  34556  cdlema1N  34557  cdlema2N  34558  paddasslem2  34587  paddasslem15  34600  paddasslem16  34601  pmodlem1  34612  pmod2iN  34615  hlmod1i  34622  atmod2i1  34627  atmod2i2  34628  atmod3i1  34630  atmod3i2  34631  atmod4i1  34632  atmod4i2  34633  llnexchb2  34635  dalawlem3  34639  dalawlem4  34640  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem9  34645  dalawlem11  34647  dalawlem13  34649  dalawlem15  34651  osumcllem7N  34728  osumcllem9N  34730  osumcllem11N  34732  pl42lem1N  34745  4atex  34842  4atex2-0aOLDN  34844  4atex2-0bOLDN  34845  4atex2-0cOLDN  34846  trlval4  34955  cdlemc5  34962  cdlemd5  34969  cdlemd6  34970  cdleme00a  34976  cdleme3g  35001  cdleme3h  35002  cdleme3  35004  cdleme4  35005  cdleme4a  35006  cdleme16aN  35026  cdleme11c  35028  cdleme11g  35032  cdleme11h  35033  cdleme12  35038  cdleme0nex  35057  cdleme18a  35058  cdleme18b  35059  cdleme18c  35060  cdleme18d  35062  cdleme20zN  35068  cdleme20y  35069  cdleme20yOLD  35070  cdleme19a  35071  cdleme19b  35072  cdleme19d  35074  cdleme19e  35075  cdleme20aN  35077  cdleme20c  35079  cdleme20d  35080  cdleme20i  35085  cdleme20j  35086  cdleme20l1  35088  cdleme20l2  35089  cdleme20m  35091  cdleme21b  35094  cdleme21c  35095  cdleme21j  35104  cdleme22aa  35107  cdleme22a  35108  cdleme22eALTN  35113  cdleme26e  35127  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme27N  35137  cdleme28a  35138  cdleme28b  35139  cdleme30a  35146  cdlemefs45eN  35199  cdleme32c  35211  cdleme32e  35213  cdleme35h  35224  cdleme36a  35228  cdleme36m  35229  cdleme37m  35230  cdleme41sn3aw  35242  cdleme41sn4aw  35243  cdleme41fva11  35245  cdleme42k  35252  cdleme43cN  35259  cdleme43dN  35260  cdleme46f2g1  35262  cdlemeg47rv2  35278  cdlemeg46sfg  35288  cdlemeg46fjgN  35289  cdlemeg46rjgN  35290  cdlemeg46fjv  35291  cdlemeg46frv  35293  cdlemeg46vrg  35295  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemeg46gfv  35298  cdleme50trn2a  35318  cdlemg2fv2  35368  cdlemg4a  35376  cdlemg4e  35382  cdlemg4f  35383  cdlemg8b  35396  cdlemg8c  35397  cdlemg9a  35400  cdlemg9b  35401  cdlemg9  35402  cdlemg10a  35408  cdlemg12a  35411  cdlemg12b  35412  cdlemg12c  35413  cdlemg12  35418  cdlemg17dN  35431  cdlemg17dALTN  35432  cdlemg17e  35433  cdlemg17i  35437  cdlemg17ir  35438  cdlemg17pq  35440  cdlemg17bq  35441  cdlemg17iqN  35442  cdlemg17  35445  cdlemg18b  35447  cdlemg18c  35448  cdlemg18d  35449  cdlemg18  35450  cdlemg19  35452  cdlemg21  35454  cdlemg28a  35461  cdlemg31b0a  35463  cdlemg33b0  35469  cdlemg35  35481  cdlemg44a  35499  cdlemh  35585  cdlemi2  35587  cdlemj1  35589  cdlemk5a  35603  cdlemk5  35604  cdlemki  35609  cdlemkvcl  35610  cdlemk10  35611  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemk15  35623  cdlemk16a  35624  cdlemk16  35625  cdlemk5u  35629  cdlemk6u  35630  cdlemk18  35636  cdlemk19  35637  cdlemk7u  35638  cdlemk11u  35639  cdlemk12u  35640  cdlemk21N  35641  cdlemk20  35642  cdlemkoatnle-2N  35643  cdlemk13-2N  35644  cdlemkole-2N  35645  cdlemk14-2N  35646  cdlemk15-2N  35647  cdlemk16-2N  35648  cdlemk17-2N  35649  cdlemk18-2N  35654  cdlemk19-2N  35655  cdlemk22  35661  cdlemk30  35662  cdlemk28-3  35676  cdlemk33N  35677  cdlemkfid1N  35689  cdlemkid1  35690  cdlemky  35694  cdlemk11ta  35697  cdlemk35s-id  35706  cdlemk39s-id  35708  cdlemk47  35717  cdlemk48  35718  cdlemk49  35719  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemk53a  35723  cdlemk53b  35724  cdlemk53  35725  cdlemk54  35726  cdlemk55a  35727  cdlemkyyN  35730  cdlemk43N  35731  cdlemk55u1  35733  cdlemk55u  35734  cdlemk39u1  35735  cdlemk19u1  35737  cdleml1N  35744  cdleml2N  35745  cdleml3N  35746  dia2dimlem6  35838  cdlemn2  35964  cdlemn2a  35965  cdlemn5pre  35969  cdlemn11pre  35979  dihjustlem  35985  dihjust  35986  dihmeetlem15N  36090  lclkrlem2y  36300  relexpxpnnidm  37476
  Copyright terms: Public domain W3C validator