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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 484 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 1134 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1087
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 206  df-an 398  df-3an 1089
This theorem is referenced by:  simp12l  1286  simp22l  1292  simp32l  1298  fsnunf  7089  f1oiso2  7255  fpr3g  8132  omeulem2  8445  uniinqs  8617  unxpdomlem3  9073  gruina  10624  dedekind  11188  addid2  11208  subaddmulsub  11488  dmdcan  11735  xaddass  13033  xaddass2  13034  xlt2add  13044  xmulasslem3  13070  xadddi2  13081  xadddi2r  13082  expaddzlem  13876  expaddz  13877  expmulz  13879  expdiv  13884  expmordi  13935  modexp  14003  pfxeq  14458  ccatopth2  14479  swrdco  14599  o1add  15372  o1mul  15373  o1sub  15374  fsumsplitsnun  15516  ntrivcvgmul  15663  prmexpb  16474  pcpremul  16593  pcdiv  16602  pcqmul  16603  pcqdiv  16607  4sqlem12  16706  f1ocpbllem  17284  ercpbl  17309  erlecpbl  17310  latjlej12  18222  latmlem12  18238  latj4  18256  latj4rot  18257  gsumsgrpccat  18527  gsmsymgreqlem2  19088  symgsssg  19124  symgfisg  19125  mndodcong  19199  cmn4  19455  ablsub4  19463  abladdsub4  19464  lsm4  19510  abvdom  20147  abvres  20148  abvtrivd  20149  lspsnvs  20425  lspsneu  20434  lspfixed  20439  lspexch  20440  lsmcv  20452  lspsolvlem  20453  coe1sclmulfv  21503  matvscacell  21634  m1detdiag  21795  cramerimplem3  21883  cnprest  22489  hausnei2  22553  isreg2  22577  cmpcld  22602  llyrest  22685  nllyrest  22686  elptr  22773  basqtop  22911  hausflimlem  23179  tmdgsum  23295  utop2nei  23451  trcfilu  23495  ssblps  23624  ssbl  23625  prdsxmslem2  23734  tgqioo  24012  metnrm  24074  bndth  24170  ncvspi  24369  ncvs1  24370  cph2ass  24426  lmmbr2  24472  iscau3  24491  bcthlem5  24541  ovolunlem2  24711  dvres2  25125  dvfsumlem2  25240  plyadd  25427  plymul  25428  coeeu  25435  coemullem  25460  aalioulem4  25544  mulcxp  25889  cxplea  25900  cxple2  25901  cxplt2  25902  cxpcn3lem  25949  angcan  26001  ang180lem5  26012  divsqrtsumlem  26178  logexprlim  26422  dchrvmasumlema  26697  dchrisum0lema  26711  logdivsum  26730  log2sumbnd  26741  abvcxp  26812  padicabv  26827  tghilberti2  27048  brbtwn2  27322  axcontlem4  27384  axcontlem8  27388  clwlkl1loop  28200  clwwlknonex2lem2  28521  clwlknon2num  28781  numclwlk1lem2  28783  chscllem4  30051  orngmul  31551  measxun2  32227  measun  32228  mbfmco2  32281  probun  32435  satfv1fvfmla1  33434  nolesgn2ores  33924  nosupres  33959  nosupbnd1lem1  33960  nosupbnd1lem2  33961  nosupbnd1lem4  33963  nosupbnd1lem5  33964  nosupbnd1lem6  33965  noinffv  33973  noinfres  33974  noinfbnd1lem1  33975  noinfbnd1lem2  33976  noinfbnd1lem4  33978  noinfbnd1lem6  33980  nosupinfsep  33984  scutbdaylt  34061  cgrcomim  34340  cgrcoml  34347  cgrcomr  34348  cgrdegen  34355  btwnintr  34370  btwnexch3  34371  btwnouttr2  34373  btwnouttr  34375  btwnexch  34376  btwndiff  34378  lineid  34434  idinside  34435  btwnconn1lem7  34444  btwnconn1lem8  34445  btwnconn1lem9  34446  btwnconn1lem12  34449  btwnconn1lem14  34451  btwnconn3  34454  midofsegid  34455  segcon2  34456  brsegle2  34460  btwnoutside  34476  outsideoftr  34480  outsideofeu  34482  linethru  34504  cnres2  35969  heibor  36027  lsmsat  37222  lkrlsp  37316  lkrlsp2  37317  lkrlsp3  37318  latm4  37447  omlspjN  37475  hlatj4  37588  4noncolr3  37667  4noncolr2  37668  4noncolr1  37669  athgt  37670  3dimlem3a  37674  3dimlem4a  37677  3dimlem4  37678  3dimlem4OLDN  37679  3dim3  37683  1cvratex  37687  hlatexch4  37695  3atlem4  37700  atcvrlln2  37733  atcvrlln  37734  lplnnlelln  37757  lvoli2  37795  lvolnlelln  37798  lvolnlelpln  37799  4atlem11b  37822  4atlem12b  37825  2lplnja  37833  2lplnj  37834  dalemyeo  37846  dath2  37951  lncvrat  37996  cdlemblem  38007  cdlemb  38008  elpaddri  38016  padd4N  38054  llnmod2i2  38077  llnexchb2  38083  dalawlem1  38085  dalawlem2  38086  pclfinN  38114  osumcllem6N  38175  pexmidlem3N  38186  lhp2lt  38215  lhp2at0  38246  lhp2atnle  38247  lhp2atne  38248  lhp2at0nle  38249  lhp2at0ne  38250  lhpelim  38251  lhpmod2i2  38252  lhpmod6i1  38253  lhple  38256  lhpat  38257  lhpat3  38260  ltrncoelN  38357  ltrncoat  38358  ltrncnv  38360  trlat  38383  trl0  38384  ltrnnidn  38388  trlnid  38393  cdlemd7  38418  cdleme0b  38426  cdleme0c  38427  cdleme0fN  38432  cdleme02N  38436  cdleme0ex1N  38437  cdleme0ex2N  38438  cdleme7aa  38456  cdleme7c  38459  cdleme7d  38460  cdleme7e  38461  cdleme7ga  38462  cdleme7  38463  cdleme8  38464  cdleme11a  38474  cdleme17c  38502  cdleme22gb  38508  cdlemeda  38512  cdleme20k  38533  cdleme21a  38539  cdleme21d  38544  cdleme22f2  38561  cdleme22g  38562  cdleme23a  38563  cdleme23b  38564  cdleme23c  38565  cdleme24  38566  cdleme28  38587  cdlemefrs32fva1  38615  cdlemefr32sn2aw  38618  cdlemefs32sn1aw  38628  cdleme41sn3a  38647  cdleme32fva  38651  cdleme32fva1  38652  cdleme35a  38662  cdleme35b  38664  cdleme35c  38665  cdleme35f  38668  cdleme39a  38679  cdleme42a  38685  cdleme42c  38686  cdleme42b  38692  cdleme42e  38693  cdleme42f  38694  cdleme42g  38695  cdleme42h  38696  cdleme43bN  38704  cdleme46f2g2  38707  cdleme17d2  38709  cdleme17d4  38711  cdleme48fv  38713  cdleme48fvg  38714  cdleme4gfv  38721  cdlemeg46c  38727  cdlemeg46nlpq  38731  cdlemeg46gfre  38746  cdleme48d  38749  cdlemeg49lebilem  38753  cdleme50trn2  38765  cdleme50ltrn  38771  cdleme  38774  cdlemf1  38775  cdlemf  38777  trlord  38783  ltrniotacnvval  38796  ltrniotavalbN  38798  cdlemg1cex  38802  cdlemg2dN  38804  cdlemg2ce  38806  cdlemg2fvlem  38808  cdlemg2idN  38810  cdlemg2kq  38816  cdlemg2l  38817  cdlemg2m  38818  cdlemg4b2  38824  cdlemg7fvN  38838  cdlemg8a  38841  cdlemg10bALTN  38850  cdlemg11aq  38852  cdlemg12d  38860  cdlemg13a  38865  cdlemg13  38866  cdlemg14f  38867  cdlemg14g  38868  cdlemg17a  38875  cdlemg17b  38876  cdlemg27a  38906  cdlemg31b0N  38908  cdlemg31a  38911  cdlemg31b  38912  cdlemg31c  38913  ltrnco  38933  trlcoabs  38935  trlcoabs2N  38936  trlcocnvat  38938  trlconid  38939  trlcolem  38940  trlcone  38942  cdlemg42  38943  cdlemg43  38944  cdlemg46  38949  cdlemg47  38950  tendoeq1  38978  tendoco2  38982  tendoplco2  38993  tendopltp  38994  cdlemh1  39029  cdlemh2  39030  cdlemi1  39032  cdlemi  39034  cdlemk1  39045  cdlemk2  39046  cdlemk3  39047  cdlemk4  39048  cdlemk8  39052  cdlemk9  39053  cdlemk9bN  39054  cdlemk31  39110  cdlemk32  39111  cdlemk28-3  39122  cdlemk19u  39184  cdlemk56w  39187  tendoex  39189  erngdvlem4  39205  erngdvlem4-rN  39213  dia11N  39262  dib11N  39374  cdlemn6  39416  cdlemn7  39417  cdlemn8  39418  cdlemn9  39419  dihordlem6  39427  dihordlem7  39428  dihord1  39432  dihord2a  39433  dihord2b  39434  dihord2pre  39439  dihord2pre2  39440  dihlsscpre  39448  dihvalcq2  39461  dihopelvalcpre  39462  dihord4  39472  dihord6b  39474  dihmeetlem1N  39504  dihglblem3N  39509  dihmeetlem2N  39513  dihglbcpreN  39514  dihmeetcN  39516  dihmeetbclemN  39518  dihmeetlem4preN  39520  dihjatc1  39525  dihjatc2N  39526  dihjatc3  39527  dihmeetlem9N  39529  dihmeetlem13N  39533  dihmeetlem20N  39540  dih1dimatlem0  39542  mapdpglem24  39918  mapdpglem32  39919  baerlem3lem2  39924  baerlem5alem2  39925  baerlem5blem2  39926  mapdh9aOLDN  40004  hdmap14lem6  40087  nnadddir  40495  sn-addid2  40582  mzpsubst  40765  pellexlem5  40850  pellex  40852  pell14qrexpclnn0  40883  pellfundex  40903  qirropth  40925  monotuz  40959  congtr  40983  congmul  40985  congsub  40988  mzpcong  40990  fzmaxdif  40999  jm2.15nn0  41021  idomsubgmo  41219  iunrelexpmin1  41529  iunrelexpmin2  41533  trclimalb2  41547  mnringmulrcld  42059  fourierdlem42  43919  fourierdlem48  43924  fourierdlem80  43956  smfaddlem1  44531  prmdvdsfmtnof1lem1  45280  uspgropssxp  45550  lidldomn1  45723  rngccatidALTV  45791  coe1sclmulval  45970  lincdifsn  46009  seposep  46463  iscnrm3rlem8  46485  iscnrm3llem2  46488
  Copyright terms: Public domain W3C validator