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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 472 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 1103 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  simpl2l  1134  simpr2l  1140  simp12l  1194  simp22l  1200  simp32l  1206  funprgOLD  5979  fsnunf  6492  f1oiso2  6642  omeulem2  7708  uniinqs  7870  unxpdomlem3  8207  gruina  9678  dedekind  10238  addid2  10257  dmdcan  10773  xaddass  12117  xaddass2  12118  xlt2add  12128  xmulasslem3  12154  xadddi2  12165  xadddi2r  12166  expaddzlem  12943  expaddz  12944  expmulz  12946  expdiv  12951  modexp  13039  ccatopth2  13517  swrdco  13629  o1add  14388  o1mul  14389  o1sub  14390  fsumsplitsnun  14528  ntrivcvgmul  14678  prmexpb  15477  pcpremul  15595  pcdiv  15604  pcqmul  15605  pcqdiv  15609  4sqlem12  15707  f1ocpbllem  16231  ercpbl  16256  erlecpbl  16257  latjlej12  17114  latmlem12  17130  latj4  17148  latj4rot  17149  symgsssg  17933  symgfisg  17934  mndodcong  18007  cmn4  18258  ablsub4  18264  abladdsub4  18265  lsm4  18309  abvdom  18886  abvres  18887  abvtrivd  18888  lspsnvs  19162  lspsneu  19171  lspfixed  19176  lspexch  19177  lsmcv  19189  lspsolvlem  19190  coe1sclmulfv  19701  matvscacell  20290  m1detdiag  20451  cramerimplem3  20539  cnprest  21141  hausnei2  21205  isreg2  21229  cmpcld  21253  llyrest  21336  nllyrest  21337  elptr  21424  basqtop  21562  hausflimlem  21830  tmdgsum  21946  utop2nei  22101  trcfilu  22145  ssblps  22274  ssbl  22275  prdsxmslem2  22381  tgqioo  22650  metnrm  22712  bndth  22804  ncvspi  23002  ncvs1  23003  cph2ass  23059  lmmbr2  23103  iscau3  23122  bcthlem5  23171  ovolunlem2  23312  dvres2  23721  dvfsumlem2  23835  plyadd  24018  plymul  24019  coeeu  24026  coemullem  24051  aalioulem4  24135  mulcxp  24476  cxplea  24487  cxple2  24488  cxplt2  24489  cxpcn3lem  24533  angcan  24577  ang180lem5  24588  divsqrtsumlem  24751  logexprlim  24995  dchrvmasumlema  25234  dchrisum0lema  25248  logdivsum  25267  log2sumbnd  25278  abvcxp  25349  padicabv  25364  tghilberti2  25578  brbtwn2  25830  axcontlem4  25892  axcontlem8  25896  clwlkl1loop  26734  clwwlkel  27009  clwwlknonex2lem2  27083  chscllem4  28627  orngmul  29931  measxun2  30401  measun  30402  mbfmco2  30455  probun  30609  nolesgn2ores  31950  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem2  31980  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd1lem6  31984  scutbdaylt  32047  cgrcomim  32221  cgrcoml  32228  cgrcomr  32229  cgrdegen  32236  btwnintr  32251  btwnexch3  32252  btwnouttr2  32254  btwnouttr  32256  btwnexch  32257  btwndiff  32259  lineid  32315  idinside  32316  btwnconn1lem7  32325  btwnconn1lem8  32326  btwnconn1lem9  32327  btwnconn1lem12  32330  btwnconn1lem14  32332  btwnconn3  32335  midofsegid  32336  segcon2  32337  brsegle2  32341  btwnoutside  32357  outsideoftr  32361  outsideofeu  32363  linethru  32385  cnres2  33692  heibor  33750  lsmsat  34613  lkrlsp  34707  lkrlsp2  34708  lkrlsp3  34709  latm4  34838  omlspjN  34866  hlatj4  34978  4noncolr3  35057  4noncolr2  35058  4noncolr1  35059  athgt  35060  3dimlem3a  35064  3dimlem4a  35067  3dimlem4  35068  3dimlem4OLDN  35069  3dim3  35073  1cvratex  35077  hlatexch4  35085  3atlem4  35090  atcvrlln2  35123  atcvrlln  35124  lplnnlelln  35147  lvoli2  35185  lvolnlelln  35188  lvolnlelpln  35189  4atlem11b  35212  4atlem12b  35215  2lplnja  35223  2lplnj  35224  dalemyeo  35236  dath2  35341  lncvrat  35386  cdlemblem  35397  cdlemb  35398  elpaddri  35406  padd4N  35444  llnmod2i2  35467  llnexchb2  35473  dalawlem1  35475  dalawlem2  35476  pclfinN  35504  osumcllem6N  35565  pexmidlem3N  35576  lhp2lt  35605  lhp2at0  35636  lhp2atnle  35637  lhp2atne  35638  lhp2at0nle  35639  lhp2at0ne  35640  lhpelim  35641  lhpmod2i2  35642  lhpmod6i1  35643  lhple  35646  lhpat  35647  lhpat3  35650  ltrncoelN  35747  ltrncoat  35748  ltrncnv  35750  trlat  35774  trl0  35775  ltrnnidn  35779  trlnid  35784  cdlemd7  35809  cdleme0b  35817  cdleme0c  35818  cdleme0fN  35823  cdleme02N  35827  cdleme0ex1N  35828  cdleme0ex2N  35829  cdleme7aa  35847  cdleme7c  35850  cdleme7d  35851  cdleme7e  35852  cdleme7ga  35853  cdleme7  35854  cdleme8  35855  cdleme11a  35865  cdleme17c  35893  cdleme22gb  35899  cdlemeda  35903  cdleme20k  35924  cdleme21a  35930  cdleme21d  35935  cdleme22f2  35952  cdleme22g  35953  cdleme23a  35954  cdleme23b  35955  cdleme23c  35956  cdleme24  35957  cdleme28  35978  cdlemefrs32fva1  36006  cdlemefr32sn2aw  36009  cdlemefs32sn1aw  36019  cdleme41sn3a  36038  cdleme32fva  36042  cdleme32fva1  36043  cdleme35a  36053  cdleme35b  36055  cdleme35c  36056  cdleme35f  36059  cdleme39a  36070  cdleme42a  36076  cdleme42c  36077  cdleme42b  36083  cdleme42e  36084  cdleme42f  36085  cdleme42g  36086  cdleme42h  36087  cdleme43bN  36095  cdleme46f2g2  36098  cdleme17d2  36100  cdleme17d4  36102  cdleme48fv  36104  cdleme48fvg  36105  cdleme4gfv  36112  cdlemeg46c  36118  cdlemeg46nlpq  36122  cdlemeg46gfre  36137  cdleme48d  36140  cdlemeg49lebilem  36144  cdleme50trn2  36156  cdleme50ltrn  36162  cdleme  36165  cdlemf1  36166  cdlemf  36168  trlord  36174  ltrniotacnvval  36187  ltrniotavalbN  36189  cdlemg1cex  36193  cdlemg2dN  36195  cdlemg2ce  36197  cdlemg2fvlem  36199  cdlemg2idN  36201  cdlemg2kq  36207  cdlemg2l  36208  cdlemg2m  36209  cdlemg4b2  36215  cdlemg7fvN  36229  cdlemg8a  36232  cdlemg10bALTN  36241  cdlemg11aq  36243  cdlemg12d  36251  cdlemg13a  36256  cdlemg13  36257  cdlemg14f  36258  cdlemg14g  36259  cdlemg17a  36266  cdlemg17b  36267  cdlemg27a  36297  cdlemg31b0N  36299  cdlemg31a  36302  cdlemg31b  36303  cdlemg31c  36304  ltrnco  36324  trlcoabs  36326  trlcoabs2N  36327  trlcocnvat  36329  trlconid  36330  trlcolem  36331  trlcone  36333  cdlemg42  36334  cdlemg43  36335  cdlemg46  36340  cdlemg47  36341  tendoeq1  36369  tendoco2  36373  tendoplco2  36384  tendopltp  36385  cdlemh1  36420  cdlemh2  36421  cdlemi1  36423  cdlemi  36425  cdlemk1  36436  cdlemk2  36437  cdlemk3  36438  cdlemk4  36439  cdlemk8  36443  cdlemk9  36444  cdlemk9bN  36445  cdlemk31  36501  cdlemk32  36502  cdlemk28-3  36513  cdlemk19u  36575  cdlemk56w  36578  tendoex  36580  erngdvlem4  36596  erngdvlem4-rN  36604  dia11N  36654  dib11N  36766  cdlemn6  36808  cdlemn7  36809  cdlemn8  36810  cdlemn9  36811  dihordlem6  36819  dihordlem7  36820  dihord1  36824  dihord2a  36825  dihord2b  36826  dihord2pre  36831  dihord2pre2  36832  dihlsscpre  36840  dihvalcq2  36853  dihopelvalcpre  36854  dihord4  36864  dihord6b  36866  dihmeetlem1N  36896  dihglblem3N  36901  dihmeetlem2N  36905  dihglbcpreN  36906  dihmeetcN  36908  dihmeetbclemN  36910  dihmeetlem4preN  36912  dihjatc1  36917  dihjatc2N  36918  dihjatc3  36919  dihmeetlem9N  36921  dihmeetlem13N  36925  dihmeetlem20N  36932  dih1dimatlem0  36934  mapdpglem24  37310  mapdpglem32  37311  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  mapdh9aOLDN  37397  hdmap14lem6  37482  mzpsubst  37628  pellexlem5  37714  pellex  37716  pell14qrexpclnn0  37747  pellfundex  37767  qirropth  37790  monotuz  37823  expmordi  37829  congtr  37849  congmul  37851  congsub  37854  mzpcong  37856  fzmaxdif  37865  jm2.15nn0  37887  idomsubgmo  38093  iunrelexpmin1  38317  iunrelexpmin2  38321  trclimalb2  38335  fourierdlem42  40684  fourierdlem48  40689  fourierdlem80  40721  smfaddlem1  41292  prmdvdsfmtnof1lem1  41821  uspgropssxp  42077  lidldomn1  42246  rngccatidALTV  42314  coe1sclmulval  42498  lincdifsn  42538
  Copyright terms: Public domain W3C validator