Theorem simp2r 1250

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 473	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1157	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

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:  simpl2rOLD  1293  simpr2rOLD  1305  simp12r  1379  simp22r  1385  simp32r  1391  fsnunf  6672  f1oiso2  6822  fnsuppres  7553  omeulem2  7896  uniinqs  8058  unxpdomlem3  8401  sup0  8607  fin23lem11  9420  reclem3pr  10152  dedekind  10481  addid2  10500  dmdcan  11016  xaddass2  12294  xlt2add  12304  xadddi2  12341  expaddzlem  13122  expaddz  13123  expmulz  13125  expdiv  13130  ccatopth2  13691  relexpaddnn  14010  o1add  14563  o1mul  14564  o1sub  14565  ntrivcvgmul  14851  prmexpb  15643  pcpremul  15761  pcdiv  15770  pcqmul  15771  pcqdiv  15775  4sqlem12  15873  f1ocpbllem  16385  ercpbl  16410  erlecpbl  16411  latjlej12  17268  latmlem12  17284  latj4  17302  symgsssg  18084  symgfisg  18085  mndodcong  18158  cmn4  18409  ablsub4  18415  abladdsub4  18416  lsm4  18460  abvdom  19038  abvtrivd  19040  lspsnvs  19317  lspsneu  19326  lspfixed  19331  lspfixedOLD  19332  lspexch  19333  lsmcv  19345  lspsolvlem  19346  mvrf1  19630  coe1sclmulfv  19857  m1detdiag  20610  cnprest  21303  isreg2  21391  elptr  21586  hausflimlem  21992  trcfilu  22307  ssblps  22436  ssbl  22437  prdsxmslem2  22543  tgqioo  22812  metnrm  22874  bndth  22966  ncvspi  23164  cph2ass  23221  iscau3  23284  ovolunlem2  23475  dvres2  23886  dvfsumlem2  24000  dvfsum2  24007  deg1tm  24088  plyadd  24183  plymul  24184  coeeu  24191  coemullem  24216  aalioulem4  24300  cxplea  24652  cxple2  24653  cxplt2  24654  cxple2a  24655  cxpcn3lem  24698  angcan  24742  ang180lem5  24753  divsqrtsumlem  24916  logexprlim  25160  dchrvmasumlema  25399  dchrisum0lema  25413  logdivsum  25432  log2sumbnd  25443  padicabv  25529  tghilberti2  25743  brbtwn2  25995  axcontlem4  26057  axcontlem8  26061  clwlkl1loop  26903  clwwlknonex2lem2  27273  chscllem4  28823  mdslmd4i  29516  orngmul  30124  nexple  30392  measxun2  30594  measun  30595  mbfmco2  30648  probun  30802  wsuclem  32086  frrlem4  32099  nolesgn2ores  32141  nolt02o  32161  noetalem5  32183  scutbdaylt  32238  cgrcomim  32412  cgrcoml  32419  cgrcomr  32420  cgrdegen  32427  btwnintr  32442  btwnexch3  32443  btwnouttr  32447  btwnexch  32448  btwndiff  32450  ifscgr  32467  lineid  32506  btwnconn1lem7  32516  btwnconn1lem8  32517  btwnconn1lem9  32518  btwnconn1lem12  32521  midofsegid  32527  brsegle2  32532  btwnoutside  32548  outsideoftr  32552  cnres2  33868  heibor  33926  lsmsat  34783  lkrlsp  34877  lkrlsp2  34878  lkrlsp3  34879  lshpkrlem6  34890  latm4  35008  omlspjN  35036  hlatj4  35149  4noncolr3  35228  4noncolr2  35229  4noncolr1  35230  3dimlem3a  35235  3dimlem4a  35238  3dimlem4  35239  3dimlem4OLDN  35240  1cvratex  35248  hlatexch4  35256  3atlem4  35261  atcvrlln2  35294  atcvrlln  35295  llnmlplnN  35314  lplnnlelln  35318  lvoli2  35356  lvolnlelln  35359  lvolnlelpln  35360  4atlem11b  35383  4atlem12b  35386  2lplnj  35395  dalemzeo  35408  dath2  35512  lncvrat  35557  cdlemb  35569  elpaddri  35577  padd4N  35615  llnmod2i2  35638  llnexchb2  35644  dalawlem1  35646  dalawlem2  35647  osumcllem6N  35736  pexmidlem3N  35747  pexmidlem4N  35748  lhp2lt  35776  lhp2at0  35807  lhp2atne  35809  lhp2at0ne  35811  lhpmod2i2  35813  lhpmod6i1  35814  lhpat  35818  lhpat3  35821  4atexlemex6  35849  ltrncoval  35920  ltrncnv  35921  ltrnnidn  35949  cdlemd7  35979  cdleme0b  35987  cdleme0c  35988  cdleme0fN  35993  cdleme0ex1N  35998  cdleme7d  36021  cdleme7e  36022  cdleme7ga  36023  cdleme7  36024  cdleme11a  36035  cdleme17c  36063  cdleme22gb  36069  cdlemeda  36073  cdleme20k  36094  cdleme21a  36100  cdleme21at  36103  cdleme21d  36105  cdleme22f2  36122  cdleme22g  36123  cdleme24  36127  cdleme28  36148  cdlemefrs29cpre1  36173  cdlemefr29exN  36177  cdlemefr32sn2aw  36179  cdleme32fva  36212  cdleme32fva1  36213  cdleme35a  36223  cdleme42c  36247  cdleme42e  36254  cdleme42f  36255  cdleme42g  36256  cdleme42h  36257  cdleme43bN  36265  cdleme46f2g2  36268  cdleme17d2  36270  cdleme4gfv  36282  cdlemeg46c  36288  cdlemeg46nlpq  36292  cdlemeg46gfre  36307  cdlemeg49lebilem  36314  cdleme50trn1  36324  cdleme50trn2  36326  cdleme50ltrn  36332  cdleme  36335  cdlemf1  36336  cdlemf  36338  trlord  36344  ltrniotavalbN  36359  cdlemg1cex  36363  cdlemg2dN  36365  cdlemg2ce  36367  cdlemg2fvlem  36369  cdlemg2idN  36371  cdlemg2kq  36377  cdlemg2l  36378  cdlemg7fvN  36399  cdlemg7aN  36400  cdlemg8a  36402  cdlemg11aq  36413  cdlemg12d  36421  cdlemg13a  36426  cdlemg13  36427  cdlemg14f  36428  cdlemg14g  36429  cdlemg17b  36437  cdlemg27a  36467  cdlemg31b0N  36469  cdlemg31a  36472  cdlemg31b  36473  cdlemg31c  36474  ltrnco  36494  trlcoabs2N  36497  trlcocnvat  36499  trlconid  36500  trlcolem  36501  cdlemg42  36504  cdlemg43  36505  cdlemg47a  36509  cdlemg46  36510  cdlemg47  36511  tendoeq1  36539  tendocoval  36541  tendoco2  36543  tendoplco2  36554  tendopltp  36555  cdlemh1  36590  cdlemh2  36591  cdlemi1  36593  cdlemi  36595  cdlemk1  36606  cdlemk2  36607  cdlemk3  36608  cdlemk4  36609  cdlemk8  36613  cdlemk9  36614  cdlemk9bN  36615  cdlemk31  36671  cdlemk28-3  36683  cdlemk19xlem  36717  cdlemk39u  36743  cdlemk19u  36745  cdlemk56w  36748  cdlemn7  36978  cdlemn8  36979  cdlemn9  36980  dihordlem6  36988  dihordlem7  36989  dihordlem7b  36990  dihord1  36993  dihord2a  36994  dihord11c  36999  dihord2pre  37000  dihord2pre2  37001  dihlsscpre  37009  dihord4  37033  dihord6b  37035  dihmeetlem2N  37074  dihglbcpreN  37075  dihmeetcN  37077  dihmeetbclemN  37079  dihmeetlem3N  37080  dihmeetlem9N  37090  dihmeetlem13N  37094  dihmeetlem20N  37101  mapdpglem24  37479  mapdpglem32  37480  baerlem3lem2  37485  baerlem5alem2  37486  baerlem5blem2  37487  mapdh9aOLDN  37565  hdmap14lem6  37648  mzpmfp  37806  mzpsubst  37807  pellexlem5  37893  pell14qrexpclnn0  37926  pellfundex  37946  qirropth  37968  monotuz  38001  expmordi  38007  congmul  38029  congsub  38032  mzpcong  38034  fzmaxdif  38043  jm2.15nn0  38065  idomsubgmo  38271  trclimalb2  38512  fourierdlem42  40839  fourierdlem48  40844  fourierdlem80  40876  prmdvdsfmtnof1lem1  42065  lidldomn1  42483  rngccatidALTV  42551  ringccatidALTV  42614  coe1sclmulval  42735