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

Theorem simp2l 1079
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2l ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 471 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 1075 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simpl2l  1106  simpr2l  1112  simp12l  1166  simp22l  1172  simp32l  1178  funprgOLD  5841  fsnunf  6334  f1oiso2  6480  omeulem2  7528  uniinqs  7692  unxpdomlem3  8029  gruina  9497  dedekind  10052  addid2  10071  dmdcan  10587  xaddass  11911  xaddass2  11912  xlt2add  11922  xmulasslem3  11948  xadddi2  11959  xadddi2r  11960  expaddzlem  12723  expaddz  12724  expmulz  12726  expdiv  12731  modexp  12819  ccatopth2  13272  swrdco  13383  o1add  14141  o1mul  14142  o1sub  14143  ntrivcvgmul  14422  prmexpb  15217  pcpremul  15335  pcdiv  15344  pcqmul  15345  pcqdiv  15349  4sqlem12  15447  f1ocpbllem  15956  ercpbl  15981  erlecpbl  15982  latjlej12  16839  latmlem12  16855  latj4  16873  latj4rot  16874  symgsssg  17659  symgfisg  17660  mndodcong  17733  cmn4  17984  ablsub4  17990  abladdsub4  17991  lsm4  18035  abvdom  18610  abvres  18611  abvtrivd  18612  lspsnvs  18884  lspsneu  18893  lspfixed  18898  lspexch  18899  lsmcv  18911  lspsolvlem  18912  coe1sclmulfv  19423  matvscacell  20009  m1detdiag  20170  cramerimplem3  20258  cnprest  20851  hausnei2  20915  isreg2  20939  cmpcld  20963  llyrest  21046  nllyrest  21047  elptr  21134  basqtop  21272  hausflimlem  21541  tmdgsum  21657  utop2nei  21812  trcfilu  21856  ssblps  21985  ssbl  21986  prdsxmslem2  22092  tgqioo  22359  metnrm  22421  bndth  22513  ncvspi  22709  ncvs1  22710  cph2ass  22766  lmmbr2  22810  iscau3  22829  bcthlem5  22878  ovolunlem2  23018  dvres2  23427  dvfsumlem2  23539  plyadd  23722  plymul  23723  coeeu  23730  coemullem  23755  aalioulem4  23839  mulcxp  24176  cxplea  24187  cxple2  24188  cxplt2  24189  cxpcn3lem  24233  angcan  24277  ang180lem5  24288  divsqrtsumlem  24451  logexprlim  24695  dchrvmasumlema  24934  dchrisum0lema  24948  logdivsum  24967  log2sumbnd  24978  abvcxp  25049  padicabv  25064  tghilberti2  25279  brbtwn2  25531  axcontlem4  25593  axcontlem8  25597  1pthon  25915  clwwlkel  26115  chscllem4  27717  orngmul  28968  measxun2  29434  measun  29435  mbfmco2  29488  probun  29642  nofulllem5  30939  cgrcomim  31100  cgrcoml  31107  cgrcomr  31108  cgrdegen  31115  btwnintr  31130  btwnexch3  31131  btwnouttr2  31133  btwnouttr  31135  btwnexch  31136  btwndiff  31138  lineid  31194  idinside  31195  btwnconn1lem7  31204  btwnconn1lem8  31205  btwnconn1lem9  31206  btwnconn1lem12  31209  btwnconn1lem14  31211  btwnconn3  31214  midofsegid  31215  segcon2  31216  brsegle2  31220  btwnoutside  31236  outsideoftr  31240  outsideofeu  31242  linethru  31264  cnres2  32556  heibor  32614  lsmsat  33137  lkrlsp  33231  lkrlsp2  33232  lkrlsp3  33233  latm4  33362  omlspjN  33390  hlatj4  33502  4noncolr3  33581  4noncolr2  33582  4noncolr1  33583  athgt  33584  3dimlem3a  33588  3dimlem4a  33591  3dimlem4  33592  3dimlem4OLDN  33593  3dim3  33597  1cvratex  33601  hlatexch4  33609  3atlem4  33614  atcvrlln2  33647  atcvrlln  33648  lplnnlelln  33671  lvoli2  33709  lvolnlelln  33712  lvolnlelpln  33713  4atlem11b  33736  4atlem12b  33739  2lplnja  33747  2lplnj  33748  dalemyeo  33760  dath2  33865  lncvrat  33910  cdlemblem  33921  cdlemb  33922  elpaddri  33930  padd4N  33968  llnmod2i2  33991  llnexchb2  33997  dalawlem1  33999  dalawlem2  34000  pclfinN  34028  osumcllem6N  34089  pexmidlem3N  34100  lhp2lt  34129  lhp2at0  34160  lhp2atnle  34161  lhp2atne  34162  lhp2at0nle  34163  lhp2at0ne  34164  lhpelim  34165  lhpmod2i2  34166  lhpmod6i1  34167  lhple  34170  lhpat  34171  lhpat3  34174  ltrncoelN  34271  ltrncoat  34272  ltrncnv  34274  trlat  34298  trl0  34299  ltrnnidn  34303  trlnid  34308  cdlemd7  34333  cdleme0b  34341  cdleme0c  34342  cdleme0fN  34347  cdleme02N  34351  cdleme0ex1N  34352  cdleme0ex2N  34353  cdleme7aa  34371  cdleme7c  34374  cdleme7d  34375  cdleme7e  34376  cdleme7ga  34377  cdleme7  34378  cdleme8  34379  cdleme11a  34389  cdleme17c  34417  cdleme22gb  34423  cdlemeda  34427  cdleme20k  34449  cdleme21a  34455  cdleme21d  34460  cdleme22f2  34477  cdleme22g  34478  cdleme23a  34479  cdleme23b  34480  cdleme23c  34481  cdleme24  34482  cdleme28  34503  cdlemefrs32fva1  34531  cdlemefr32sn2aw  34534  cdlemefs32sn1aw  34544  cdleme41sn3a  34563  cdleme32fva  34567  cdleme32fva1  34568  cdleme35a  34578  cdleme35b  34580  cdleme35c  34581  cdleme35f  34584  cdleme39a  34595  cdleme42a  34601  cdleme42c  34602  cdleme42b  34608  cdleme42e  34609  cdleme42f  34610  cdleme42g  34611  cdleme42h  34612  cdleme43bN  34620  cdleme46f2g2  34623  cdleme17d2  34625  cdleme17d4  34627  cdleme48fv  34629  cdleme48fvg  34630  cdleme4gfv  34637  cdlemeg46c  34643  cdlemeg46nlpq  34647  cdlemeg46gfre  34662  cdleme48d  34665  cdlemeg49lebilem  34669  cdleme50trn2  34681  cdleme50ltrn  34687  cdleme  34690  cdlemf1  34691  cdlemf  34693  trlord  34699  ltrniotacnvval  34712  ltrniotavalbN  34714  cdlemg1cex  34718  cdlemg2dN  34720  cdlemg2ce  34722  cdlemg2fvlem  34724  cdlemg2idN  34726  cdlemg2kq  34732  cdlemg2l  34733  cdlemg2m  34734  cdlemg4b2  34740  cdlemg7fvN  34754  cdlemg8a  34757  cdlemg10bALTN  34766  cdlemg11aq  34768  cdlemg12d  34776  cdlemg13a  34781  cdlemg13  34782  cdlemg14f  34783  cdlemg14g  34784  cdlemg17a  34791  cdlemg17b  34792  cdlemg27a  34822  cdlemg31b0N  34824  cdlemg31a  34827  cdlemg31b  34828  cdlemg31c  34829  ltrnco  34849  trlcoabs  34851  trlcoabs2N  34852  trlcocnvat  34854  trlconid  34855  trlcolem  34856  trlcone  34858  cdlemg42  34859  cdlemg43  34860  cdlemg46  34865  cdlemg47  34866  tendoeq1  34894  tendoco2  34898  tendoplco2  34909  tendopltp  34910  cdlemh1  34945  cdlemh2  34946  cdlemi1  34948  cdlemi  34950  cdlemk1  34961  cdlemk2  34962  cdlemk3  34963  cdlemk4  34964  cdlemk8  34968  cdlemk9  34969  cdlemk9bN  34970  cdlemk31  35026  cdlemk32  35027  cdlemk28-3  35038  cdlemk19u  35100  cdlemk56w  35103  tendoex  35105  erngdvlem4  35121  erngdvlem4-rN  35129  dia11N  35179  dib11N  35291  cdlemn6  35333  cdlemn7  35334  cdlemn8  35335  cdlemn9  35336  dihordlem6  35344  dihordlem7  35345  dihord1  35349  dihord2a  35350  dihord2b  35351  dihord2pre  35356  dihord2pre2  35357  dihlsscpre  35365  dihvalcq2  35378  dihopelvalcpre  35379  dihord4  35389  dihord6b  35391  dihmeetlem1N  35421  dihglblem3N  35426  dihmeetlem2N  35430  dihglbcpreN  35431  dihmeetcN  35433  dihmeetbclemN  35435  dihmeetlem4preN  35437  dihjatc1  35442  dihjatc2N  35443  dihjatc3  35444  dihmeetlem9N  35446  dihmeetlem13N  35450  dihmeetlem20N  35457  dih1dimatlem0  35459  mapdpglem24  35835  mapdpglem32  35836  baerlem3lem2  35841  baerlem5alem2  35842  baerlem5blem2  35843  mapdh9aOLDN  35922  hdmap14lem6  36007  mzpsubst  36153  pellexlem5  36239  pellex  36241  pell14qrexpclnn0  36272  pellfundex  36292  qirropth  36315  monotuz  36348  expmordi  36354  congtr  36374  congmul  36376  congsub  36379  mzpcong  36381  fzmaxdif  36390  jm2.15nn0  36412  idomsubgmo  36619  iunrelexpmin1  36843  iunrelexpmin2  36847  trclimalb2  36861  fourierdlem42  38866  fourierdlem48  38871  fourierdlem80  38903  smfaddlem1  39473  prmdvdsfmtnof1lem1  39859  clwlkl1loop  41011  clwwlksel  41243  lidldomn1  41733  rngccatidALTV  41803  coe1sclmulval  41989  lincdifsn  42029
  Copyright terms: Public domain W3C validator