Theorem simp2r 1196

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp12r  1283  simp22r  1289  simp32r  1295  fsnunf  6950  f1oiso2  7108  fnsuppres  7860  omeulem2  8212  uniinqs  8380  unxpdomlem3  8727  sup0  8933  fin23lem11  9742  reclem3pr  10474  dedekind  10806  addid2  10826  subaddmulsub  11106  dmdcan  11353  xaddass2  12646  xlt2add  12656  xadddi2  12693  expaddzlem  13475  expaddz  13476  expmulz  13478  expdiv  13483  expmordi  13534  pfxeq  14061  ccatopth2  14082  relexpaddnn  14413  o1add  14973  o1mul  14974  o1sub  14975  ntrivcvgmul  15261  prmexpb  16065  pcpremul  16183  pcdiv  16192  pcqmul  16193  pcqdiv  16197  4sqlem12  16295  f1ocpbllem  16800  ercpbl  16825  erlecpbl  16826  latjlej12  17680  latmlem12  17696  latj4  17714  gsumsgrpccat  18007  symgsssg  18598  symgfisg  18599  mndodcong  18673  cmn4  18929  ablsub4  18936  abladdsub4  18937  lsm4  18983  abvdom  19612  abvtrivd  19614  lspsnvs  19889  lspsneu  19898  lspfixed  19903  lspexch  19904  lsmcv  19916  lspsolvlem  19917  mvrf1  20208  coe1sclmulfv  20454  m1detdiag  21209  cnprest  21900  isreg2  21988  elptr  22184  hausflimlem  22590  trcfilu  22906  ssblps  23035  ssbl  23036  prdsxmslem2  23142  tgqioo  23411  metnrm  23473  bndth  23565  ncvspi  23763  cph2ass  23820  iscau3  23884  ovolunlem2  24102  dvres2  24513  dvfsumlem2  24627  dvfsum2  24634  deg1tm  24715  plyadd  24810  plymul  24811  coeeu  24818  coemullem  24843  aalioulem4  24927  cxplea  25282  cxple2  25283  cxplt2  25284  cxple2a  25285  cxpcn3lem  25331  angcan  25383  ang180lem5  25394  divsqrtsumlem  25560  logexprlim  25804  dchrvmasumlema  26079  dchrisum0lema  26093  logdivsum  26112  log2sumbnd  26123  padicabv  26209  tghilberti2  26427  brbtwn2  26694  axcontlem4  26756  axcontlem8  26760  clwlkl1loop  27567  chscllem4  29420  mdslmd4i  30113  orngmul  30880  nexple  31272  measxun2  31473  measun  31474  mbfmco2  31527  probun  31681  satfv1fvfmla1  32674  wsuclem  33116  frrlem4  33130  nolesgn2ores  33183  nolt02o  33203  noetalem5  33225  scutbdaylt  33280  cgrcomim  33454  cgrcoml  33461  cgrcomr  33462  cgrdegen  33469  btwnintr  33484  btwnexch3  33485  btwnouttr  33489  btwnexch  33490  btwndiff  33492  ifscgr  33509  lineid  33548  btwnconn1lem7  33558  btwnconn1lem8  33559  btwnconn1lem9  33560  btwnconn1lem12  33563  midofsegid  33569  brsegle2  33574  btwnoutside  33590  outsideoftr  33594  cnres2  35045  heibor  35103  lsmsat  36148  lkrlsp  36242  lkrlsp2  36243  lkrlsp3  36244  lshpkrlem6  36255  latm4  36373  omlspjN  36401  hlatj4  36514  4noncolr3  36593  4noncolr2  36594  4noncolr1  36595  3dimlem3a  36600  3dimlem4a  36603  3dimlem4  36604  3dimlem4OLDN  36605  1cvratex  36613  hlatexch4  36621  3atlem4  36626  atcvrlln2  36659  atcvrlln  36660  llnmlplnN  36679  lplnnlelln  36683  lvoli2  36721  lvolnlelln  36724  lvolnlelpln  36725  4atlem11b  36748  4atlem12b  36751  2lplnj  36760  dalemzeo  36773  dath2  36877  lncvrat  36922  cdlemb  36934  elpaddri  36942  padd4N  36980  llnmod2i2  37003  llnexchb2  37009  dalawlem1  37011  dalawlem2  37012  osumcllem6N  37101  pexmidlem3N  37112  pexmidlem4N  37113  lhp2lt  37141  lhp2at0  37172  lhp2atne  37174  lhp2at0ne  37176  lhpmod2i2  37178  lhpmod6i1  37179  lhpat  37183  lhpat3  37186  4atexlemex6  37214  ltrncoval  37285  ltrncnv  37286  ltrnnidn  37314  cdlemd7  37344  cdleme0b  37352  cdleme0c  37353  cdleme0fN  37358  cdleme0ex1N  37363  cdleme7d  37386  cdleme7e  37387  cdleme7ga  37388  cdleme7  37389  cdleme11a  37400  cdleme17c  37428  cdleme22gb  37434  cdlemeda  37438  cdleme20k  37459  cdleme21a  37465  cdleme21at  37468  cdleme21d  37470  cdleme22f2  37487  cdleme22g  37488  cdleme24  37492  cdleme28  37513  cdlemefrs29cpre1  37538  cdlemefr29exN  37542  cdlemefr32sn2aw  37544  cdleme32fva  37577  cdleme32fva1  37578  cdleme35a  37588  cdleme42c  37612  cdleme42e  37619  cdleme42f  37620  cdleme42g  37621  cdleme42h  37622  cdleme43bN  37630  cdleme46f2g2  37633  cdleme17d2  37635  cdleme4gfv  37647  cdlemeg46c  37653  cdlemeg46nlpq  37657  cdlemeg46gfre  37672  cdlemeg49lebilem  37679  cdleme50trn1  37689  cdleme50trn2  37691  cdleme50ltrn  37697  cdleme  37700  cdlemf1  37701  cdlemf  37703  trlord  37709  ltrniotavalbN  37724  cdlemg1cex  37728  cdlemg2dN  37730  cdlemg2ce  37732  cdlemg2fvlem  37734  cdlemg2idN  37736  cdlemg2kq  37742  cdlemg2l  37743  cdlemg7fvN  37764  cdlemg7aN  37765  cdlemg8a  37767  cdlemg11aq  37778  cdlemg12d  37786  cdlemg13a  37791  cdlemg13  37792  cdlemg14f  37793  cdlemg14g  37794  cdlemg17b  37802  cdlemg27a  37832  cdlemg31b0N  37834  cdlemg31a  37837  cdlemg31b  37838  cdlemg31c  37839  ltrnco  37859  trlcoabs2N  37862  trlcocnvat  37864  trlconid  37865  trlcolem  37866  cdlemg42  37869  cdlemg43  37870  cdlemg47a  37874  cdlemg46  37875  cdlemg47  37876  tendoeq1  37904  tendocoval  37906  tendoco2  37908  tendoplco2  37919  tendopltp  37920  cdlemh1  37955  cdlemh2  37956  cdlemi1  37958  cdlemi  37960  cdlemk1  37971  cdlemk2  37972  cdlemk3  37973  cdlemk4  37974  cdlemk8  37978  cdlemk9  37979  cdlemk9bN  37980  cdlemk31  38036  cdlemk28-3  38048  cdlemk19xlem  38082  cdlemk39u  38108  cdlemk19u  38110  cdlemk56w  38113  cdlemn7  38343  cdlemn8  38344  cdlemn9  38345  dihordlem6  38353  dihordlem7  38354  dihordlem7b  38355  dihord1  38358  dihord2a  38359  dihord11c  38364  dihord2pre  38365  dihord2pre2  38366  dihlsscpre  38374  dihord4  38398  dihord6b  38400  dihmeetlem2N  38439  dihglbcpreN  38440  dihmeetcN  38442  dihmeetbclemN  38444  dihmeetlem3N  38445  dihmeetlem9N  38455  dihmeetlem13N  38459  dihmeetlem20N  38466  mapdpglem24  38844  mapdpglem32  38845  baerlem3lem2  38850  baerlem5alem2  38851  baerlem5blem2  38852  mapdh9aOLDN  38930  hdmap14lem6  39013  nnadddir  39169  sn-addid2  39240  mzpmfp  39350  mzpsubst  39351  pellexlem5  39436  pell14qrexpclnn0  39469  pellfundex  39489  qirropth  39511  monotuz  39544  congmul  39570  congsub  39573  mzpcong  39575  fzmaxdif  39584  jm2.15nn0  39606  idomsubgmo  39804  trclimalb2  40077  fourierdlem42  42441  fourierdlem48  42446  fourierdlem80  42478  prmdvdsfmtnof1lem1  43753  lidldomn1  44199  rngccatidALTV  44267  ringccatidALTV  44330  coe1sclmulval  44446  line2  44746  line2xlem  44747  line2x  44748  line2y  44749  itsclc0yqsol  44758