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

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

Proof of Theorem simp31
StepHypRef Expression
1 simp1 1131 . 2 ((𝜒𝜃𝜏) → 𝜒)
213ad2ant3 1130 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 1074
This theorem is referenced by:  simpl31OLD  1328  simpr31OLD  1346  simp131  1393  simp231  1402  simp331  1411  smogt  7634  frlmphl  20342  mdetuni0  20649  mdetmul  20651  gsummatr01lem3  20685  decpmatmullem  20798  tsmsxp  22179  log2sumbnd  25453  ax5seg  26038  wlkoniswlk  26788  iocinioc2  29871  totprob  30819  eqfunresadj  31987  nosupres  32180  cgrtr  32426  cgrtr3  32428  ofscom  32441  cgrextend  32442  segconeq  32444  ifscgr  32478  btwnxfr  32490  colinearxfr  32509  brofs2  32511  brifs2  32512  fscgr  32514  btwnconn1lem1  32521  btwnconn1lem2  32522  btwnconn1lem5  32525  btwnconn1lem6  32526  btwnconn1lem7  32527  btwnconn1lem8  32528  btwnconn1lem9  32529  btwnconn1lem10  32530  btwnconn1lem11  32531  btwnconn1lem12  32532  seglecgr12im  32544  seglecgr12  32545  segletr  32548  outsideofeq  32564  ivthALT  32657  lshpkrlem5  34922  lshpkrlem6  34923  exatleN  35211  atbtwn  35253  atbtwnexOLDN  35254  atbtwnex  35255  4noncolr3  35260  3dimlem3a  35267  3dimlem4a  35270  3dim1  35274  3dim2  35275  1cvrat  35283  2atjlej  35286  hlatexch4  35288  ps-2b  35289  2atm  35334  2atmat  35368  4atlem11b  35415  4atlem11  35416  4at  35420  4at2  35421  2lplnja  35426  2lplnj  35427  dalemswapyz  35463  dalemccnedd  35494  cdlemb  35601  paddasslem5  35631  paddasslem15  35641  pmodlem1  35653  dalawlem1  35678  dalawlem3  35680  dalawlem4  35681  dalawlem5  35682  dalawlem6  35683  dalawlem7  35684  dalawlem8  35685  dalawlem9  35686  dalawlem11  35688  dalawlem12  35689  dalawlem15  35692  osumcllem5N  35767  osumcllem6N  35768  lhpexle3lem  35818  lhpmcvr4N  35833  lhpmcvr6N  35835  4atex2  35884  4atex2-0bOLDN  35886  4atex3  35888  ltrn11at  35954  trlval3  35995  cdlemd3  36008  cdleme0moN  36033  cdleme7aa  36050  cdleme7b  36052  cdleme7c  36053  cdleme7d  36054  cdleme7e  36055  cdleme7ga  36056  cdleme7  36057  cdleme16aN  36067  cdleme11dN  36070  cdleme11e  36071  cdleme11l  36077  cdleme11  36078  cdleme12  36079  cdleme14  36081  cdleme15b  36083  cdleme15c  36084  cdleme16b  36087  cdleme16c  36088  cdleme16d  36089  cdleme16e  36090  cdleme16f  36091  cdleme17c  36096  cdleme18c  36101  cdleme18d  36103  cdlemeda  36106  cdleme19a  36111  cdleme19b  36112  cdleme19c  36113  cdleme20aN  36117  cdleme20bN  36118  cdleme20d  36120  cdleme20i  36125  cdleme20j  36126  cdleme20l1  36128  cdleme20l2  36129  cdleme21d  36138  cdleme21e  36139  cdleme21f  36140  cdleme22aa  36147  cdleme22e  36152  cdleme22eALTN  36153  cdleme22f2  36155  cdleme22g  36156  cdleme23b  36158  cdleme26eALTN  36169  cdleme26fALTN  36170  cdleme26f  36171  cdleme26f2ALTN  36172  cdleme26f2  36173  cdleme28a  36178  cdleme28b  36179  cdleme32b  36250  cdleme32c  36251  cdleme32e  36253  cdleme35h  36264  cdleme35sn2aw  36266  cdleme41sn3aw  36282  cdleme41sn4aw  36283  cdlemeg46gfre  36340  cdlemf1  36369  cdlemg1cex  36396  cdlemg2ce  36400  cdlemg4d  36421  cdlemg4e  36422  cdlemg4f  36423  cdlemg4  36425  cdlemg6d  36429  cdlemg6e  36430  cdlemg7fvN  36432  cdlemg8b  36436  cdlemg8c  36437  cdlemg9a  36440  cdlemg9b  36441  cdlemg9  36442  cdlemg11aq  36446  cdlemg10a  36448  cdlemg12a  36451  cdlemg12b  36452  cdlemg12c  36453  cdlemg12d  36454  cdlemg13  36460  cdlemg14f  36461  cdlemg14g  36462  cdlemg17b  36470  cdlemg17dN  36471  cdlemg17e  36473  cdlemg17i  36477  cdlemg17pq  36480  cdlemg17iqN  36482  cdlemg18c  36488  cdlemg18d  36489  cdlemg18  36490  cdlemg19  36492  cdlemg21  36494  cdlemg27a  36500  cdlemg31b0N  36502  cdlemg27b  36504  cdlemg31c  36507  cdlemg33b0  36509  cdlemg33c0  36510  cdlemg33  36519  cdlemg35  36521  cdlemg43  36538  cdlemg44a  36539  cdlemg46  36543  cdlemh2  36624  cdlemh  36625  cdlemj1  36629  cdlemk3  36641  cdlemk5  36644  cdlemk6  36645  cdlemki  36649  cdlemksv2  36655  cdlemk12  36658  cdlemk15  36663  cdlemk16  36665  cdlemk18  36676  cdlemk19  36677  cdlemk7u  36678  cdlemk12u  36680  cdlemkoatnle-2N  36683  cdlemk13-2N  36684  cdlemkole-2N  36685  cdlemk14-2N  36686  cdlemk15-2N  36687  cdlemk16-2N  36688  cdlemk17-2N  36689  cdlemk18-2N  36694  cdlemk19-2N  36695  cdlemk7u-2N  36696  cdlemk11u-2N  36697  cdlemk12u-2N  36698  cdlemk20-2N  36700  cdlemk22  36701  cdlemk30  36702  cdlemk31  36704  cdlemk24-3  36711  cdlemkid2  36732  cdlemkfid3N  36733  cdlemk11ta  36737  cdlemkid3N  36741  cdlemk11tc  36753  cdlemk45  36755  cdlemk46  36756  cdlemk47  36757  cdlemk52  36762  cdlemk53a  36763  cdlemk53b  36764  cdleml1N  36784  cdleml3N  36786  cdlemn7  37012  cdlemn10  37015  dihordlem7  37023  dihord1  37027  dihord11c  37033  dihord2  37036  hlhilphllem  37771  fmuldfeq  40336
  Copyright terms: Public domain W3C validator