Theorem simp2r 1081

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2r	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 476	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1076	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl2r  1108  simpr2r  1114  simp12r  1168  simp22r  1174  simp32r  1180  funprgOLD  5855  fsnunf  6356  f1oiso2  6502  fnsuppres  7209  omeulem2  7550  uniinqs  7714  unxpdomlem3  8051  sup0  8255  fin23lem11  9022  reclem3pr  9750  dedekind  10079  addid2  10098  dmdcan  10614  xaddass2  11952  xlt2add  11962  xadddi2  11999  expaddzlem  12765  expaddz  12766  expmulz  12768  expdiv  12773  ccatopth2  13323  relexpaddnn  13639  o1add  14192  o1mul  14193  o1sub  14194  ntrivcvgmul  14473  prmexpb  15268  pcpremul  15386  pcdiv  15395  pcqmul  15396  pcqdiv  15400  4sqlem12  15498  f1ocpbllem  16007  ercpbl  16032  erlecpbl  16033  latjlej12  16890  latmlem12  16906  latj4  16924  symgsssg  17710  symgfisg  17711  mndodcong  17784  cmn4  18035  ablsub4  18041  abladdsub4  18042  lsm4  18086  abvdom  18661  abvtrivd  18663  lspsnvs  18935  lspsneu  18944  lspfixed  18949  lspexch  18950  lsmcv  18962  lspsolvlem  18963  mvrf1  19246  coe1sclmulfv  19474  m1detdiag  20222  cnprest  20903  isreg2  20991  elptr  21186  hausflimlem  21593  trcfilu  21908  ssblps  22037  ssbl  22038  prdsxmslem2  22144  tgqioo  22411  metnrm  22473  bndth  22565  ncvspi  22764  cph2ass  22821  iscau3  22884  ovolunlem2  23073  dvres2  23482  dvfsumlem2  23594  dvfsum2  23601  deg1tm  23682  plyadd  23777  plymul  23778  coeeu  23785  coemullem  23810  aalioulem4  23894  cxplea  24242  cxple2  24243  cxplt2  24244  cxple2a  24245  cxpcn3lem  24288  angcan  24332  ang180lem5  24343  divsqrtsumlem  24506  logexprlim  24750  dchrvmasumlema  24989  dchrisum0lema  25003  logdivsum  25022  log2sumbnd  25033  padicabv  25119  tghilberti2  25333  brbtwn2  25585  axcontlem4  25647  axcontlem8  25651  1pthon  26121  chscllem4  27883  mdslmd4i  28576  orngmul  29134  nexple  29399  measxun2  29600  measun  29601  mbfmco2  29654  probun  29808  wsuclem  31017  wsuclemOLD  31018  cgrcomim  31266  cgrcoml  31273  cgrcomr  31274  cgrdegen  31281  btwnintr  31296  btwnexch3  31297  btwnouttr  31301  btwnexch  31302  btwndiff  31304  ifscgr  31321  lineid  31360  btwnconn1lem7  31370  btwnconn1lem8  31371  btwnconn1lem9  31372  btwnconn1lem12  31375  midofsegid  31381  brsegle2  31386  btwnoutside  31402  outsideoftr  31406  cnres2  32732  heibor  32790  lsmsat  33313  lkrlsp  33407  lkrlsp2  33408  lkrlsp3  33409  lshpkrlem6  33420  latm4  33538  omlspjN  33566  hlatj4  33678  4noncolr3  33757  4noncolr2  33758  4noncolr1  33759  3dimlem3a  33764  3dimlem4a  33767  3dimlem4  33768  3dimlem4OLDN  33769  1cvratex  33777  hlatexch4  33785  3atlem4  33790  atcvrlln2  33823  atcvrlln  33824  llnmlplnN  33843  lplnnlelln  33847  lvoli2  33885  lvolnlelln  33888  lvolnlelpln  33889  4atlem11b  33912  4atlem12b  33915  2lplnj  33924  dalemzeo  33937  dath2  34041  lncvrat  34086  cdlemb  34098  elpaddri  34106  padd4N  34144  llnmod2i2  34167  llnexchb2  34173  dalawlem1  34175  dalawlem2  34176  osumcllem6N  34265  pexmidlem3N  34276  pexmidlem4N  34277  lhp2lt  34305  lhp2at0  34336  lhp2atne  34338  lhp2at0ne  34340  lhpmod2i2  34342  lhpmod6i1  34343  lhpat  34347  lhpat3  34350  4atexlemex6  34378  ltrncoval  34449  ltrncnv  34450  ltrnnidn  34479  cdlemd7  34509  cdleme0b  34517  cdleme0c  34518  cdleme0fN  34523  cdleme0ex1N  34528  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme11a  34565  cdleme17c  34593  cdleme22gb  34599  cdlemeda  34603  cdleme20k  34625  cdleme21a  34631  cdleme21at  34634  cdleme21d  34636  cdleme22f2  34653  cdleme22g  34654  cdleme24  34658  cdleme28  34679  cdlemefrs29cpre1  34704  cdlemefr29exN  34708  cdlemefr32sn2aw  34710  cdleme32fva  34743  cdleme32fva1  34744  cdleme35a  34754  cdleme42c  34778  cdleme42e  34785  cdleme42f  34786  cdleme42g  34787  cdleme42h  34788  cdleme43bN  34796  cdleme46f2g2  34799  cdleme17d2  34801  cdleme4gfv  34813  cdlemeg46c  34819  cdlemeg46nlpq  34823  cdlemeg46gfre  34838  cdlemeg49lebilem  34845  cdleme50trn1  34855  cdleme50trn2  34857  cdleme50ltrn  34863  cdleme  34866  cdlemf1  34867  cdlemf  34869  trlord  34875  ltrniotavalbN  34890  cdlemg1cex  34894  cdlemg2dN  34896  cdlemg2ce  34898  cdlemg2fvlem  34900  cdlemg2idN  34902  cdlemg2kq  34908  cdlemg2l  34909  cdlemg7fvN  34930  cdlemg7aN  34931  cdlemg8a  34933  cdlemg11aq  34944  cdlemg12d  34952  cdlemg13a  34957  cdlemg13  34958  cdlemg14f  34959  cdlemg14g  34960  cdlemg17b  34968  cdlemg27a  34998  cdlemg31b0N  35000  cdlemg31a  35003  cdlemg31b  35004  cdlemg31c  35005  ltrnco  35025  trlcoabs2N  35028  trlcocnvat  35030  trlconid  35031  trlcolem  35032  cdlemg42  35035  cdlemg43  35036  cdlemg47a  35040  cdlemg46  35041  cdlemg47  35042  tendoeq1  35070  tendocoval  35072  tendoco2  35074  tendoplco2  35085  tendopltp  35086  cdlemh1  35121  cdlemh2  35122  cdlemi1  35124  cdlemi  35126  cdlemk1  35137  cdlemk2  35138  cdlemk3  35139  cdlemk4  35140  cdlemk8  35144  cdlemk9  35145  cdlemk9bN  35146  cdlemk31  35202  cdlemk28-3  35214  cdlemk19xlem  35248  cdlemk39u  35274  cdlemk19u  35276  cdlemk56w  35279  cdlemn7  35510  cdlemn8  35511  cdlemn9  35512  dihordlem6  35520  dihordlem7  35521  dihordlem7b  35522  dihord1  35525  dihord2a  35526  dihord11c  35531  dihord2pre  35532  dihord2pre2  35533  dihlsscpre  35541  dihord4  35565  dihord6b  35567  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetcN  35609  dihmeetbclemN  35611  dihmeetlem3N  35612  dihmeetlem9N  35622  dihmeetlem13N  35626  dihmeetlem20N  35633  mapdpglem24  36011  mapdpglem32  36012  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  mapdh9aOLDN  36098  hdmap14lem6  36183  mzpmfp  36328  mzpsubst  36329  pellexlem5  36415  pell14qrexpclnn0  36448  pellfundex  36468  qirropth  36491  monotuz  36524  expmordi  36530  congmul  36552  congsub  36555  mzpcong  36557  fzmaxdif  36566  jm2.15nn0  36588  idomsubgmo  36795  trclimalb2  37037  fourierdlem42  39042  fourierdlem48  39047  fourierdlem80  39079  prmdvdsfmtnof1lem1  40034  clwlkl1loop  40989  lidldomn1  41711  rngccatidALTV  41781  ringccatidALTV  41844  coe1sclmulval  41967