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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 475 . 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:  simpl2r  1107  simpr2r  1113  simp12r  1167  simp22r  1173  simp32r  1179  funprgOLD  5840  fsnunf  6333  f1oiso2  6479  fnsuppres  7186  omeulem2  7527  uniinqs  7691  unxpdomlem3  8028  sup0  8232  fin23lem11  8999  reclem3pr  9727  dedekind  10051  addid2  10070  dmdcan  10586  xaddass2  11911  xlt2add  11921  xadddi2  11958  expaddzlem  12722  expaddz  12723  expmulz  12725  expdiv  12730  ccatopth2  13271  relexpaddnn  13587  o1add  14140  o1mul  14141  o1sub  14142  ntrivcvgmul  14421  prmexpb  15216  pcpremul  15334  pcdiv  15343  pcqmul  15344  pcqdiv  15348  4sqlem12  15446  f1ocpbllem  15955  ercpbl  15980  erlecpbl  15981  latjlej12  16838  latmlem12  16854  latj4  16872  symgsssg  17658  symgfisg  17659  mndodcong  17732  cmn4  17983  ablsub4  17989  abladdsub4  17990  lsm4  18034  abvdom  18609  abvtrivd  18611  lspsnvs  18883  lspsneu  18892  lspfixed  18897  lspexch  18898  lsmcv  18910  lspsolvlem  18911  mvrf1  19194  coe1sclmulfv  19422  m1detdiag  20169  cnprest  20850  isreg2  20938  elptr  21133  hausflimlem  21540  trcfilu  21855  ssblps  21984  ssbl  21985  prdsxmslem2  22091  tgqioo  22358  metnrm  22420  bndth  22512  ncvspi  22708  cph2ass  22765  iscau3  22828  ovolunlem2  23017  dvres2  23426  dvfsumlem2  23538  dvfsum2  23545  deg1tm  23626  plyadd  23721  plymul  23722  coeeu  23729  coemullem  23754  aalioulem4  23838  cxplea  24186  cxple2  24187  cxplt2  24188  cxple2a  24189  cxpcn3lem  24232  angcan  24276  ang180lem5  24287  divsqrtsumlem  24450  logexprlim  24694  dchrvmasumlema  24933  dchrisum0lema  24947  logdivsum  24966  log2sumbnd  24977  padicabv  25063  tghilberti2  25278  brbtwn2  25530  axcontlem4  25592  axcontlem8  25596  1pthon  25914  chscllem4  27676  mdslmd4i  28369  orngmul  28927  nexple  29192  measxun2  29393  measun  29394  mbfmco2  29447  probun  29601  wsuclem  30810  wsuclemOLD  30811  cgrcomim  31059  cgrcoml  31066  cgrcomr  31067  cgrdegen  31074  btwnintr  31089  btwnexch3  31090  btwnouttr  31094  btwnexch  31095  btwndiff  31097  ifscgr  31114  lineid  31153  btwnconn1lem7  31163  btwnconn1lem8  31164  btwnconn1lem9  31165  btwnconn1lem12  31168  midofsegid  31174  brsegle2  31179  btwnoutside  31195  outsideoftr  31199  cnres2  32515  heibor  32573  lsmsat  33096  lkrlsp  33190  lkrlsp2  33191  lkrlsp3  33192  lshpkrlem6  33203  latm4  33321  omlspjN  33349  hlatj4  33461  4noncolr3  33540  4noncolr2  33541  4noncolr1  33542  3dimlem3a  33547  3dimlem4a  33550  3dimlem4  33551  3dimlem4OLDN  33552  1cvratex  33560  hlatexch4  33568  3atlem4  33573  atcvrlln2  33606  atcvrlln  33607  llnmlplnN  33626  lplnnlelln  33630  lvoli2  33668  lvolnlelln  33671  lvolnlelpln  33672  4atlem11b  33695  4atlem12b  33698  2lplnj  33707  dalemzeo  33720  dath2  33824  lncvrat  33869  cdlemb  33881  elpaddri  33889  padd4N  33927  llnmod2i2  33950  llnexchb2  33956  dalawlem1  33958  dalawlem2  33959  osumcllem6N  34048  pexmidlem3N  34059  pexmidlem4N  34060  lhp2lt  34088  lhp2at0  34119  lhp2atne  34121  lhp2at0ne  34123  lhpmod2i2  34125  lhpmod6i1  34126  lhpat  34130  lhpat3  34133  4atexlemex6  34161  ltrncoval  34232  ltrncnv  34233  ltrnnidn  34262  cdlemd7  34292  cdleme0b  34300  cdleme0c  34301  cdleme0fN  34306  cdleme0ex1N  34311  cdleme7d  34334  cdleme7e  34335  cdleme7ga  34336  cdleme7  34337  cdleme11a  34348  cdleme17c  34376  cdleme22gb  34382  cdlemeda  34386  cdleme20k  34408  cdleme21a  34414  cdleme21at  34417  cdleme21d  34419  cdleme22f2  34436  cdleme22g  34437  cdleme24  34441  cdleme28  34462  cdlemefrs29cpre1  34487  cdlemefr29exN  34491  cdlemefr32sn2aw  34493  cdleme32fva  34526  cdleme32fva1  34527  cdleme35a  34537  cdleme42c  34561  cdleme42e  34568  cdleme42f  34569  cdleme42g  34570  cdleme42h  34571  cdleme43bN  34579  cdleme46f2g2  34582  cdleme17d2  34584  cdleme4gfv  34596  cdlemeg46c  34602  cdlemeg46nlpq  34606  cdlemeg46gfre  34621  cdlemeg49lebilem  34628  cdleme50trn1  34638  cdleme50trn2  34640  cdleme50ltrn  34646  cdleme  34649  cdlemf1  34650  cdlemf  34652  trlord  34658  ltrniotavalbN  34673  cdlemg1cex  34677  cdlemg2dN  34679  cdlemg2ce  34681  cdlemg2fvlem  34683  cdlemg2idN  34685  cdlemg2kq  34691  cdlemg2l  34692  cdlemg7fvN  34713  cdlemg7aN  34714  cdlemg8a  34716  cdlemg11aq  34727  cdlemg12d  34735  cdlemg13a  34740  cdlemg13  34741  cdlemg14f  34742  cdlemg14g  34743  cdlemg17b  34751  cdlemg27a  34781  cdlemg31b0N  34783  cdlemg31a  34786  cdlemg31b  34787  cdlemg31c  34788  ltrnco  34808  trlcoabs2N  34811  trlcocnvat  34813  trlconid  34814  trlcolem  34815  cdlemg42  34818  cdlemg43  34819  cdlemg47a  34823  cdlemg46  34824  cdlemg47  34825  tendoeq1  34853  tendocoval  34855  tendoco2  34857  tendoplco2  34868  tendopltp  34869  cdlemh1  34904  cdlemh2  34905  cdlemi1  34907  cdlemi  34909  cdlemk1  34920  cdlemk2  34921  cdlemk3  34922  cdlemk4  34923  cdlemk8  34927  cdlemk9  34928  cdlemk9bN  34929  cdlemk31  34985  cdlemk28-3  34997  cdlemk19xlem  35031  cdlemk39u  35057  cdlemk19u  35059  cdlemk56w  35062  cdlemn7  35293  cdlemn8  35294  cdlemn9  35295  dihordlem6  35303  dihordlem7  35304  dihordlem7b  35305  dihord1  35308  dihord2a  35309  dihord11c  35314  dihord2pre  35315  dihord2pre2  35316  dihlsscpre  35324  dihord4  35348  dihord6b  35350  dihmeetlem2N  35389  dihglbcpreN  35390  dihmeetcN  35392  dihmeetbclemN  35394  dihmeetlem3N  35395  dihmeetlem9N  35405  dihmeetlem13N  35409  dihmeetlem20N  35416  mapdpglem24  35794  mapdpglem32  35795  baerlem3lem2  35800  baerlem5alem2  35801  baerlem5blem2  35802  mapdh9aOLDN  35881  hdmap14lem6  35966  mzpmfp  36111  mzpsubst  36112  pellexlem5  36198  pell14qrexpclnn0  36231  pellfundex  36251  qirropth  36274  monotuz  36307  expmordi  36313  congmul  36335  congsub  36338  mzpcong  36340  fzmaxdif  36349  jm2.15nn0  36371  idomsubgmo  36578  trclimalb2  36820  fourierdlem42  38825  fourierdlem48  38830  fourierdlem80  38862  prmdvdsfmtnof1lem1  39818  clwlkl1loop  40970  lidldomn1  41692  rngccatidALTV  41762  ringccatidALTV  41825  coe1sclmulval  41948
  Copyright terms: Public domain W3C validator