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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 485 . 2 ((𝜓𝜒) → 𝜒)
213ad2ant2 1134 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 397  df-3an 1089
This theorem is referenced by:  simp12r  1287  simp22r  1293  simp32r  1299  fsnunf  7127  f1oiso2  7293  fnsuppres  8118  frrlem4  8216  omeulem2  8526  uniinqs  8732  unxpdomlem3  9192  sup0  9398  fin23lem11  10249  reclem3pr  10981  dedekind  11314  addid2  11334  subaddmulsub  11614  dmdcan  11861  xaddass2  13161  xlt2add  13171  xadddi2  13208  expaddzlem  14003  expaddz  14004  expmulz  14006  expdiv  14011  expmordi  14064  pfxeq  14576  ccatopth2  14597  relexpaddnn  14928  o1add  15488  o1mul  15489  o1sub  15490  ntrivcvgmul  15779  prmexpb  16588  pcpremul  16707  pcdiv  16716  pcqmul  16717  pcqdiv  16721  4sqlem12  16820  f1ocpbllem  17398  ercpbl  17423  erlecpbl  17424  latjlej12  18336  latmlem12  18352  latj4  18370  gsumsgrpccat  18642  symgsssg  19240  symgfisg  19241  mndodcong  19315  cmn4  19574  ablsub4  19582  abladdsub4  19583  lsm4  19629  abvdom  20282  abvtrivd  20284  lspsnvs  20560  lspsneu  20569  lspfixed  20574  lspexch  20575  lsmcv  20587  lspsolvlem  20588  mvrf1  21378  coe1sclmulfv  21638  m1detdiag  21930  cnprest  22624  isreg2  22712  elptr  22908  hausflimlem  23314  trcfilu  23630  ssblps  23759  ssbl  23760  prdsxmslem2  23869  tgqioo  24147  metnrm  24209  bndth  24305  ncvspi  24504  cph2ass  24561  iscau3  24626  ovolunlem2  24846  dvres2  25260  dvfsumlem2  25375  dvfsum2  25382  deg1tm  25467  plyadd  25562  plymul  25563  coeeu  25570  coemullem  25595  aalioulem4  25679  cxplea  26035  cxple2  26036  cxplt2  26037  cxple2a  26038  cxpcn3lem  26084  angcan  26136  ang180lem5  26147  divsqrtsumlem  26313  logexprlim  26557  dchrvmasumlema  26832  dchrisum0lema  26846  logdivsum  26865  log2sumbnd  26876  padicabv  26962  nolesgn2ores  27004  nogesgn1o  27005  nogesgn1ores  27006  nolt02o  27027  nogt01o  27028  nosupinfsep  27064  noetalem1  27073  noeta2  27108  scutbdaylt  27141  tghilberti2  27466  brbtwn2  27740  axcontlem4  27802  axcontlem8  27806  clwlkl1loop  28617  chscllem4  30468  mdslmd4i  31161  orngmul  31981  nexple  32477  measxun2  32678  measun  32679  mbfmco2  32734  probun  32888  satfv1fvfmla1  33886  wsuclem  34270  cgrcomim  34541  cgrcoml  34548  cgrcomr  34549  cgrdegen  34556  btwnintr  34571  btwnexch3  34572  btwnouttr  34576  btwnexch  34577  btwndiff  34579  ifscgr  34596  lineid  34635  btwnconn1lem7  34645  btwnconn1lem8  34646  btwnconn1lem9  34647  btwnconn1lem12  34650  midofsegid  34656  brsegle2  34661  btwnoutside  34677  outsideoftr  34681  cnres2  36189  heibor  36247  lsmsat  37437  lkrlsp  37531  lkrlsp2  37532  lkrlsp3  37533  lshpkrlem6  37544  latm4  37662  omlspjN  37690  hlatj4  37803  4noncolr3  37883  4noncolr2  37884  4noncolr1  37885  3dimlem3a  37890  3dimlem4a  37893  3dimlem4  37894  3dimlem4OLDN  37895  1cvratex  37903  hlatexch4  37911  3atlem4  37916  atcvrlln2  37949  atcvrlln  37950  llnmlplnN  37969  lplnnlelln  37973  lvoli2  38011  lvolnlelln  38014  lvolnlelpln  38015  4atlem11b  38038  4atlem12b  38041  2lplnj  38050  dalemzeo  38063  dath2  38167  lncvrat  38212  cdlemb  38224  elpaddri  38232  padd4N  38270  llnmod2i2  38293  llnexchb2  38299  dalawlem1  38301  dalawlem2  38302  osumcllem6N  38391  pexmidlem3N  38402  pexmidlem4N  38403  lhp2lt  38431  lhp2at0  38462  lhp2atne  38464  lhp2at0ne  38466  lhpmod2i2  38468  lhpmod6i1  38469  lhpat  38473  lhpat3  38476  4atexlemex6  38504  ltrncoval  38575  ltrncnv  38576  ltrnnidn  38604  cdlemd7  38634  cdleme0b  38642  cdleme0c  38643  cdleme0fN  38648  cdleme0ex1N  38653  cdleme7d  38676  cdleme7e  38677  cdleme7ga  38678  cdleme7  38679  cdleme11a  38690  cdleme17c  38718  cdleme22gb  38724  cdlemeda  38728  cdleme20k  38749  cdleme21a  38755  cdleme21at  38758  cdleme21d  38760  cdleme22f2  38777  cdleme22g  38778  cdleme24  38782  cdleme28  38803  cdlemefrs29cpre1  38828  cdlemefr29exN  38832  cdlemefr32sn2aw  38834  cdleme32fva  38867  cdleme32fva1  38868  cdleme35a  38878  cdleme42c  38902  cdleme42e  38909  cdleme42f  38910  cdleme42g  38911  cdleme42h  38912  cdleme43bN  38920  cdleme46f2g2  38923  cdleme17d2  38925  cdleme4gfv  38937  cdlemeg46c  38943  cdlemeg46nlpq  38947  cdlemeg46gfre  38962  cdlemeg49lebilem  38969  cdleme50trn1  38979  cdleme50trn2  38981  cdleme50ltrn  38987  cdleme  38990  cdlemf1  38991  cdlemf  38993  trlord  38999  ltrniotavalbN  39014  cdlemg1cex  39018  cdlemg2dN  39020  cdlemg2ce  39022  cdlemg2fvlem  39024  cdlemg2idN  39026  cdlemg2kq  39032  cdlemg2l  39033  cdlemg7fvN  39054  cdlemg7aN  39055  cdlemg8a  39057  cdlemg11aq  39068  cdlemg12d  39076  cdlemg13a  39081  cdlemg13  39082  cdlemg14f  39083  cdlemg14g  39084  cdlemg17b  39092  cdlemg27a  39122  cdlemg31b0N  39124  cdlemg31a  39127  cdlemg31b  39128  cdlemg31c  39129  ltrnco  39149  trlcoabs2N  39152  trlcocnvat  39154  trlconid  39155  trlcolem  39156  cdlemg42  39159  cdlemg43  39160  cdlemg47a  39164  cdlemg46  39165  cdlemg47  39166  tendoeq1  39194  tendocoval  39196  tendoco2  39198  tendoplco2  39209  tendopltp  39210  cdlemh1  39245  cdlemh2  39246  cdlemi1  39248  cdlemi  39250  cdlemk1  39261  cdlemk2  39262  cdlemk3  39263  cdlemk4  39264  cdlemk8  39268  cdlemk9  39269  cdlemk9bN  39270  cdlemk31  39326  cdlemk28-3  39338  cdlemk19xlem  39372  cdlemk39u  39398  cdlemk19u  39400  cdlemk56w  39403  cdlemn7  39633  cdlemn8  39634  cdlemn9  39635  dihordlem6  39643  dihordlem7  39644  dihordlem7b  39645  dihord1  39648  dihord2a  39649  dihord11c  39654  dihord2pre  39655  dihord2pre2  39656  dihlsscpre  39664  dihord4  39688  dihord6b  39690  dihmeetlem2N  39729  dihglbcpreN  39730  dihmeetcN  39732  dihmeetbclemN  39734  dihmeetlem3N  39735  dihmeetlem9N  39745  dihmeetlem13N  39749  dihmeetlem20N  39756  mapdpglem24  40134  mapdpglem32  40135  baerlem3lem2  40140  baerlem5alem2  40141  baerlem5blem2  40142  mapdh9aOLDN  40220  hdmap14lem6  40303  nnadddir  40724  sn-addid2  40811  mzpmfp  41008  mzpsubst  41009  pellexlem5  41094  pell14qrexpclnn0  41127  pellfundex  41147  qirropth  41169  monotuz  41203  congmul  41229  congsub  41232  mzpcong  41234  fzmaxdif  41243  jm2.15nn0  41265  idomsubgmo  41463  trclimalb2  41940  mnringmulrcld  42450  fourierdlem42  44322  fourierdlem48  44327  fourierdlem80  44359  prmdvdsfmtnof1lem1  45708  lidldomn1  46151  rngccatidALTV  46219  ringccatidALTV  46282  coe1sclmulval  46398  line2  46770  line2xlem  46771  line2x  46772  line2y  46773  itsclc0yqsol  46782  seposep  46890  iscnrm3rlem8  46912  iscnrm3llem2  46915
  Copyright terms: Public domain W3C validator