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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 470 . 2 ((𝜓𝜒) → 𝜓)
213ad2ant2 1157 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simpl2lOLD  1291  simpr2lOLD  1303  simp12l  1378  simp22l  1384  simp32l  1390  fsnunf  6686  f1oiso2  6836  omeulem2  7910  uniinqs  8072  unxpdomlem3  8415  gruina  9935  dedekind  10495  addid2  10514  dmdcan  11030  xaddass  12317  xaddass2  12318  xlt2add  12328  xmulasslem3  12354  xadddi2  12365  xadddi2r  12366  expaddzlem  13146  expaddz  13147  expmulz  13149  expdiv  13154  modexp  13242  ccatopth2  13715  swrdco  13827  o1add  14587  o1mul  14588  o1sub  14589  fsumsplitsnun  14727  ntrivcvgmul  14875  prmexpb  15667  pcpremul  15785  pcdiv  15794  pcqmul  15795  pcqdiv  15799  4sqlem12  15897  f1ocpbllem  16409  ercpbl  16434  erlecpbl  16435  latjlej12  17292  latmlem12  17308  latj4  17326  latj4rot  17327  symgsssg  18108  symgfisg  18109  mndodcong  18182  cmn4  18433  ablsub4  18439  abladdsub4  18440  lsm4  18484  abvdom  19062  abvres  19063  abvtrivd  19064  lspsnvs  19341  lspsneu  19350  lspfixed  19355  lspfixedOLD  19356  lspexch  19357  lsmcv  19369  lspsolvlem  19370  coe1sclmulfv  19881  matvscacell  20473  m1detdiag  20635  cramerimplem3  20725  cnprest  21328  hausnei2  21392  isreg2  21416  cmpcld  21440  llyrest  21523  nllyrest  21524  elptr  21611  basqtop  21749  hausflimlem  22017  tmdgsum  22133  utop2nei  22288  trcfilu  22332  ssblps  22461  ssbl  22462  prdsxmslem2  22568  tgqioo  22837  metnrm  22899  bndth  22991  ncvspi  23189  ncvs1  23190  cph2ass  23246  lmmbr2  23291  iscau3  23310  bcthlem5  23359  ovolunlem2  23502  dvres2  23913  dvfsumlem2  24027  plyadd  24210  plymul  24211  coeeu  24218  coemullem  24243  aalioulem4  24327  mulcxp  24668  cxplea  24679  cxple2  24680  cxplt2  24681  cxpcn3lem  24725  angcan  24769  ang180lem5  24780  divsqrtsumlem  24943  logexprlim  25187  dchrvmasumlema  25426  dchrisum0lema  25440  logdivsum  25459  log2sumbnd  25470  abvcxp  25541  padicabv  25556  tghilberti2  25770  brbtwn2  26022  axcontlem4  26084  axcontlem8  26088  clwlkl1loop  26930  clwwlkel  27218  clwwlknonex2lem2  27300  clwlknon2num  27571  numclwlk1lem2  27573  chscllem4  28850  orngmul  30151  measxun2  30621  measun  30622  mbfmco2  30675  probun  30829  nolesgn2ores  32168  nosupres  32196  nosupbnd1lem1  32197  nosupbnd1lem2  32198  nosupbnd1lem4  32200  nosupbnd1lem5  32201  nosupbnd1lem6  32202  scutbdaylt  32265  cgrcomim  32439  cgrcoml  32446  cgrcomr  32447  cgrdegen  32454  btwnintr  32469  btwnexch3  32470  btwnouttr2  32472  btwnouttr  32474  btwnexch  32475  btwndiff  32477  lineid  32533  idinside  32534  btwnconn1lem7  32543  btwnconn1lem8  32544  btwnconn1lem9  32545  btwnconn1lem12  32548  btwnconn1lem14  32550  btwnconn3  32553  midofsegid  32554  segcon2  32555  brsegle2  32559  btwnoutside  32575  outsideoftr  32579  outsideofeu  32581  linethru  32603  cnres2  33892  heibor  33950  lsmsat  34807  lkrlsp  34901  lkrlsp2  34902  lkrlsp3  34903  latm4  35032  omlspjN  35060  hlatj4  35173  4noncolr3  35252  4noncolr2  35253  4noncolr1  35254  athgt  35255  3dimlem3a  35259  3dimlem4a  35262  3dimlem4  35263  3dimlem4OLDN  35264  3dim3  35268  1cvratex  35272  hlatexch4  35280  3atlem4  35285  atcvrlln2  35318  atcvrlln  35319  lplnnlelln  35342  lvoli2  35380  lvolnlelln  35383  lvolnlelpln  35384  4atlem11b  35407  4atlem12b  35410  2lplnja  35418  2lplnj  35419  dalemyeo  35431  dath2  35536  lncvrat  35581  cdlemblem  35592  cdlemb  35593  elpaddri  35601  padd4N  35639  llnmod2i2  35662  llnexchb2  35668  dalawlem1  35670  dalawlem2  35671  pclfinN  35699  osumcllem6N  35760  pexmidlem3N  35771  lhp2lt  35800  lhp2at0  35831  lhp2atnle  35832  lhp2atne  35833  lhp2at0nle  35834  lhp2at0ne  35835  lhpelim  35836  lhpmod2i2  35837  lhpmod6i1  35838  lhple  35841  lhpat  35842  lhpat3  35845  ltrncoelN  35942  ltrncoat  35943  ltrncnv  35945  trlat  35968  trl0  35969  ltrnnidn  35973  trlnid  35978  cdlemd7  36003  cdleme0b  36011  cdleme0c  36012  cdleme0fN  36017  cdleme02N  36021  cdleme0ex1N  36022  cdleme0ex2N  36023  cdleme7aa  36041  cdleme7c  36044  cdleme7d  36045  cdleme7e  36046  cdleme7ga  36047  cdleme7  36048  cdleme8  36049  cdleme11a  36059  cdleme17c  36087  cdleme22gb  36093  cdlemeda  36097  cdleme20k  36118  cdleme21a  36124  cdleme21d  36129  cdleme22f2  36146  cdleme22g  36147  cdleme23a  36148  cdleme23b  36149  cdleme23c  36150  cdleme24  36151  cdleme28  36172  cdlemefrs32fva1  36200  cdlemefr32sn2aw  36203  cdlemefs32sn1aw  36213  cdleme41sn3a  36232  cdleme32fva  36236  cdleme32fva1  36237  cdleme35a  36247  cdleme35b  36249  cdleme35c  36250  cdleme35f  36253  cdleme39a  36264  cdleme42a  36270  cdleme42c  36271  cdleme42b  36277  cdleme42e  36278  cdleme42f  36279  cdleme42g  36280  cdleme42h  36281  cdleme43bN  36289  cdleme46f2g2  36292  cdleme17d2  36294  cdleme17d4  36296  cdleme48fv  36298  cdleme48fvg  36299  cdleme4gfv  36306  cdlemeg46c  36312  cdlemeg46nlpq  36316  cdlemeg46gfre  36331  cdleme48d  36334  cdlemeg49lebilem  36338  cdleme50trn2  36350  cdleme50ltrn  36356  cdleme  36359  cdlemf1  36360  cdlemf  36362  trlord  36368  ltrniotacnvval  36381  ltrniotavalbN  36383  cdlemg1cex  36387  cdlemg2dN  36389  cdlemg2ce  36391  cdlemg2fvlem  36393  cdlemg2idN  36395  cdlemg2kq  36401  cdlemg2l  36402  cdlemg2m  36403  cdlemg4b2  36409  cdlemg7fvN  36423  cdlemg8a  36426  cdlemg10bALTN  36435  cdlemg11aq  36437  cdlemg12d  36445  cdlemg13a  36450  cdlemg13  36451  cdlemg14f  36452  cdlemg14g  36453  cdlemg17a  36460  cdlemg17b  36461  cdlemg27a  36491  cdlemg31b0N  36493  cdlemg31a  36496  cdlemg31b  36497  cdlemg31c  36498  ltrnco  36518  trlcoabs  36520  trlcoabs2N  36521  trlcocnvat  36523  trlconid  36524  trlcolem  36525  trlcone  36527  cdlemg42  36528  cdlemg43  36529  cdlemg46  36534  cdlemg47  36535  tendoeq1  36563  tendoco2  36567  tendoplco2  36578  tendopltp  36579  cdlemh1  36614  cdlemh2  36615  cdlemi1  36617  cdlemi  36619  cdlemk1  36630  cdlemk2  36631  cdlemk3  36632  cdlemk4  36633  cdlemk8  36637  cdlemk9  36638  cdlemk9bN  36639  cdlemk31  36695  cdlemk32  36696  cdlemk28-3  36707  cdlemk19u  36769  cdlemk56w  36772  tendoex  36774  erngdvlem4  36790  erngdvlem4-rN  36798  dia11N  36847  dib11N  36959  cdlemn6  37001  cdlemn7  37002  cdlemn8  37003  cdlemn9  37004  dihordlem6  37012  dihordlem7  37013  dihord1  37017  dihord2a  37018  dihord2b  37019  dihord2pre  37024  dihord2pre2  37025  dihlsscpre  37033  dihvalcq2  37046  dihopelvalcpre  37047  dihord4  37057  dihord6b  37059  dihmeetlem1N  37089  dihglblem3N  37094  dihmeetlem2N  37098  dihglbcpreN  37099  dihmeetcN  37101  dihmeetbclemN  37103  dihmeetlem4preN  37105  dihjatc1  37110  dihjatc2N  37111  dihjatc3  37112  dihmeetlem9N  37114  dihmeetlem13N  37118  dihmeetlem20N  37125  dih1dimatlem0  37127  mapdpglem24  37503  mapdpglem32  37504  baerlem3lem2  37509  baerlem5alem2  37510  baerlem5blem2  37511  mapdh9aOLDN  37589  hdmap14lem6  37672  mzpsubst  37831  pellexlem5  37917  pellex  37919  pell14qrexpclnn0  37950  pellfundex  37970  qirropth  37992  monotuz  38025  expmordi  38031  congtr  38051  congmul  38053  congsub  38056  mzpcong  38058  fzmaxdif  38067  jm2.15nn0  38089  idomsubgmo  38295  iunrelexpmin1  38518  iunrelexpmin2  38522  trclimalb2  38536  fourierdlem42  40863  fourierdlem48  40868  fourierdlem80  40900  smfaddlem1  41471  prmdvdsfmtnof1lem1  42089  uspgropssxp  42338  lidldomn1  42507  rngccatidALTV  42575  coe1sclmulval  42759  lincdifsn  42799
  Copyright terms: Public domain W3C validator