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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 486 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 1131 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simp12l  1283  simp22l  1289  simp32l  1295  fsnunf  6928  f1oiso2  7088  omeulem2  8196  uniinqs  8364  unxpdomlem3  8712  gruina  10233  dedekind  10796  addid2  10816  subaddmulsub  11096  dmdcan  11343  xaddass  12634  xaddass2  12635  xlt2add  12645  xmulasslem3  12671  xadddi2  12682  xadddi2r  12683  expaddzlem  13472  expaddz  13473  expmulz  13475  expdiv  13480  expmordi  13531  modexp  13599  pfxeq  14053  ccatopth2  14074  swrdco  14194  o1add  14966  o1mul  14967  o1sub  14968  fsumsplitsnun  15106  ntrivcvgmul  15254  prmexpb  16056  pcpremul  16174  pcdiv  16183  pcqmul  16184  pcqdiv  16188  4sqlem12  16286  f1ocpbllem  16793  ercpbl  16818  erlecpbl  16819  latjlej12  17673  latmlem12  17689  latj4  17707  latj4rot  17708  gsumsgrpccat  18000  gsmsymgreqlem2  18555  symgsssg  18591  symgfisg  18592  mndodcong  18666  cmn4  18922  ablsub4  18930  abladdsub4  18931  lsm4  18977  abvdom  19606  abvres  19607  abvtrivd  19608  lspsnvs  19883  lspsneu  19892  lspfixed  19897  lspexch  19898  lsmcv  19910  lspsolvlem  19911  coe1sclmulfv  20916  matvscacell  21045  m1detdiag  21206  cramerimplem3  21294  cnprest  21898  hausnei2  21962  isreg2  21986  cmpcld  22011  llyrest  22094  nllyrest  22095  elptr  22182  basqtop  22320  hausflimlem  22588  tmdgsum  22704  utop2nei  22860  trcfilu  22904  ssblps  23033  ssbl  23034  prdsxmslem2  23140  tgqioo  23409  metnrm  23471  bndth  23567  ncvspi  23765  ncvs1  23766  cph2ass  23822  lmmbr2  23867  iscau3  23886  bcthlem5  23936  ovolunlem2  24106  dvres2  24519  dvfsumlem2  24634  plyadd  24818  plymul  24819  coeeu  24826  coemullem  24851  aalioulem4  24935  mulcxp  25280  cxplea  25291  cxple2  25292  cxplt2  25293  cxpcn3lem  25340  angcan  25392  ang180lem5  25403  divsqrtsumlem  25569  logexprlim  25813  dchrvmasumlema  26088  dchrisum0lema  26102  logdivsum  26121  log2sumbnd  26132  abvcxp  26203  padicabv  26218  tghilberti2  26436  brbtwn2  26703  axcontlem4  26765  axcontlem8  26769  clwlkl1loop  27576  clwwlknonex2lem2  27897  clwlknon2num  28157  numclwlk1lem2  28159  chscllem4  29427  orngmul  30931  measxun2  31583  measun  31584  mbfmco2  31637  probun  31791  satfv1fvfmla1  32784  fpr3g  33236  nolesgn2ores  33293  nosupres  33321  nosupbnd1lem1  33322  nosupbnd1lem2  33323  nosupbnd1lem4  33325  nosupbnd1lem5  33326  nosupbnd1lem6  33327  scutbdaylt  33390  cgrcomim  33564  cgrcoml  33571  cgrcomr  33572  cgrdegen  33579  btwnintr  33594  btwnexch3  33595  btwnouttr2  33597  btwnouttr  33599  btwnexch  33600  btwndiff  33602  lineid  33658  idinside  33659  btwnconn1lem7  33668  btwnconn1lem8  33669  btwnconn1lem9  33670  btwnconn1lem12  33673  btwnconn1lem14  33675  btwnconn3  33678  midofsegid  33679  segcon2  33680  brsegle2  33684  btwnoutside  33700  outsideoftr  33704  outsideofeu  33706  linethru  33728  cnres2  35200  heibor  35258  lsmsat  36303  lkrlsp  36397  lkrlsp2  36398  lkrlsp3  36399  latm4  36528  omlspjN  36556  hlatj4  36669  4noncolr3  36748  4noncolr2  36749  4noncolr1  36750  athgt  36751  3dimlem3a  36755  3dimlem4a  36758  3dimlem4  36759  3dimlem4OLDN  36760  3dim3  36764  1cvratex  36768  hlatexch4  36776  3atlem4  36781  atcvrlln2  36814  atcvrlln  36815  lplnnlelln  36838  lvoli2  36876  lvolnlelln  36879  lvolnlelpln  36880  4atlem11b  36903  4atlem12b  36906  2lplnja  36914  2lplnj  36915  dalemyeo  36927  dath2  37032  lncvrat  37077  cdlemblem  37088  cdlemb  37089  elpaddri  37097  padd4N  37135  llnmod2i2  37158  llnexchb2  37164  dalawlem1  37166  dalawlem2  37167  pclfinN  37195  osumcllem6N  37256  pexmidlem3N  37267  lhp2lt  37296  lhp2at0  37327  lhp2atnle  37328  lhp2atne  37329  lhp2at0nle  37330  lhp2at0ne  37331  lhpelim  37332  lhpmod2i2  37333  lhpmod6i1  37334  lhple  37337  lhpat  37338  lhpat3  37341  ltrncoelN  37438  ltrncoat  37439  ltrncnv  37441  trlat  37464  trl0  37465  ltrnnidn  37469  trlnid  37474  cdlemd7  37499  cdleme0b  37507  cdleme0c  37508  cdleme0fN  37513  cdleme02N  37517  cdleme0ex1N  37518  cdleme0ex2N  37519  cdleme7aa  37537  cdleme7c  37540  cdleme7d  37541  cdleme7e  37542  cdleme7ga  37543  cdleme7  37544  cdleme8  37545  cdleme11a  37555  cdleme17c  37583  cdleme22gb  37589  cdlemeda  37593  cdleme20k  37614  cdleme21a  37620  cdleme21d  37625  cdleme22f2  37642  cdleme22g  37643  cdleme23a  37644  cdleme23b  37645  cdleme23c  37646  cdleme24  37647  cdleme28  37668  cdlemefrs32fva1  37696  cdlemefr32sn2aw  37699  cdlemefs32sn1aw  37709  cdleme41sn3a  37728  cdleme32fva  37732  cdleme32fva1  37733  cdleme35a  37743  cdleme35b  37745  cdleme35c  37746  cdleme35f  37749  cdleme39a  37760  cdleme42a  37766  cdleme42c  37767  cdleme42b  37773  cdleme42e  37774  cdleme42f  37775  cdleme42g  37776  cdleme42h  37777  cdleme43bN  37785  cdleme46f2g2  37788  cdleme17d2  37790  cdleme17d4  37792  cdleme48fv  37794  cdleme48fvg  37795  cdleme4gfv  37802  cdlemeg46c  37808  cdlemeg46nlpq  37812  cdlemeg46gfre  37827  cdleme48d  37830  cdlemeg49lebilem  37834  cdleme50trn2  37846  cdleme50ltrn  37852  cdleme  37855  cdlemf1  37856  cdlemf  37858  trlord  37864  ltrniotacnvval  37877  ltrniotavalbN  37879  cdlemg1cex  37883  cdlemg2dN  37885  cdlemg2ce  37887  cdlemg2fvlem  37889  cdlemg2idN  37891  cdlemg2kq  37897  cdlemg2l  37898  cdlemg2m  37899  cdlemg4b2  37905  cdlemg7fvN  37919  cdlemg8a  37922  cdlemg10bALTN  37931  cdlemg11aq  37933  cdlemg12d  37941  cdlemg13a  37946  cdlemg13  37947  cdlemg14f  37948  cdlemg14g  37949  cdlemg17a  37956  cdlemg17b  37957  cdlemg27a  37987  cdlemg31b0N  37989  cdlemg31a  37992  cdlemg31b  37993  cdlemg31c  37994  ltrnco  38014  trlcoabs  38016  trlcoabs2N  38017  trlcocnvat  38019  trlconid  38020  trlcolem  38021  trlcone  38023  cdlemg42  38024  cdlemg43  38025  cdlemg46  38030  cdlemg47  38031  tendoeq1  38059  tendoco2  38063  tendoplco2  38074  tendopltp  38075  cdlemh1  38110  cdlemh2  38111  cdlemi1  38113  cdlemi  38115  cdlemk1  38126  cdlemk2  38127  cdlemk3  38128  cdlemk4  38129  cdlemk8  38133  cdlemk9  38134  cdlemk9bN  38135  cdlemk31  38191  cdlemk32  38192  cdlemk28-3  38203  cdlemk19u  38265  cdlemk56w  38268  tendoex  38270  erngdvlem4  38286  erngdvlem4-rN  38294  dia11N  38343  dib11N  38455  cdlemn6  38497  cdlemn7  38498  cdlemn8  38499  cdlemn9  38500  dihordlem6  38508  dihordlem7  38509  dihord1  38513  dihord2a  38514  dihord2b  38515  dihord2pre  38520  dihord2pre2  38521  dihlsscpre  38529  dihvalcq2  38542  dihopelvalcpre  38543  dihord4  38553  dihord6b  38555  dihmeetlem1N  38585  dihglblem3N  38590  dihmeetlem2N  38594  dihglbcpreN  38595  dihmeetcN  38597  dihmeetbclemN  38599  dihmeetlem4preN  38601  dihjatc1  38606  dihjatc2N  38607  dihjatc3  38608  dihmeetlem9N  38610  dihmeetlem13N  38614  dihmeetlem20N  38621  dih1dimatlem0  38623  mapdpglem24  38999  mapdpglem32  39000  baerlem3lem2  39005  baerlem5alem2  39006  baerlem5blem2  39007  mapdh9aOLDN  39085  hdmap14lem6  39168  nnadddir  39464  sn-addid2  39535  mzpsubst  39682  pellexlem5  39767  pellex  39769  pell14qrexpclnn0  39800  pellfundex  39820  qirropth  39842  monotuz  39875  congtr  39899  congmul  39901  congsub  39904  mzpcong  39906  fzmaxdif  39915  jm2.15nn0  39937  idomsubgmo  40135  iunrelexpmin1  40402  iunrelexpmin2  40406  trclimalb2  40420  mnringmulrcld  40929  fourierdlem42  42784  fourierdlem48  42789  fourierdlem80  42821  smfaddlem1  43389  prmdvdsfmtnof1lem1  44094  uspgropssxp  44365  lidldomn1  44538  rngccatidALTV  44606  coe1sclmulval  44786  lincdifsn  44826
  Copyright terms: Public domain W3C validator