Theorem simp2r 1023

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 461	. 2
2	1	3ad2ant2 1018	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  simpl2r  1050  simpr2r  1056  simp12r  1110  simp22r  1116  simp32r  1122  funprg  5642  fsnunf  6109  f1oiso2  6248  fnsuppres  6946  omeulem2  7251  uniinqs  7410  unxpdomlem3  7746  fin23lem11  8718  reclem3pr  9448  dedekind  9765  addid2  9784  dmdcan  10279  xaddass2  11471  xlt2add  11481  xadddi2  11518  expaddzlem  12209  expaddz  12210  expmulz  12212  expdiv  12216  ccatopth2  12696  o1add  13436  o1mul  13437  o1sub  13438  ntrivcvgmul  13711  prmexpb  14258  pcpremul  14367  pcdiv  14376  pcqmul  14377  pcqdiv  14381  4sqlem12  14474  f1ocpbllem  14921  ercpbl  14946  erlecpbl  14947  latjlej12  15697  latmlem12  15713  latj4  15731  symgsssg  16492  symgfisg  16493  mndodcong  16566  cmn4  16817  ablsub4  16823  abladdsub4  16824  lsm4  16866  abvdom  17487  abvtrivd  17489  lspsnvs  17760  lspsneu  17769  lspfixed  17774  lspexch  17775  lsmcv  17787  lspsolvlem  17788  mvrf1  18081  coe1sclmulfv  18324  m1detdiag  19099  cnprest  19790  isreg2  19878  elptr  20074  hausflimlem  20480  trcfilu  20797  ssblps  20925  ssbl  20926  prdsxmslem2  21032  tgqioo  21305  metnrm  21366  bndth  21458  cph2ass  21659  iscau3  21717  ovolunlem2  21909  dvres2  22316  dvfsumlem2  22428  dvfsum2  22435  deg1tm  22519  plyadd  22614  plymul  22615  coeeu  22622  coemullem  22647  aalioulem4  22731  cxplea  23077  cxple2  23078  cxplt2  23079  cxple2a  23080  cxpcn3lem  23121  angcan  23134  ang180lem5  23145  divsqrtsumlem  23309  logexprlim  23500  dchrvmasumlema  23685  dchrisum0lema  23699  logdivsum  23718  log2sumbnd  23729  padicabv  23815  tghilbert1_2  24018  brbtwn2  24208  axcontlem4  24270  axcontlem8  24274  1pthon  24593  chscllem4  26558  mdslmd4i  27252  orngmul  27793  nexple  28005  measxun2  28181  measun  28182  mbfmco2  28236  probun  28358  wsuclem  29381  cgrcomim  29639  cgrcoml  29646  cgrcomr  29647  cgrdegen  29654  btwnintr  29669  btwnexch3  29670  btwnouttr  29674  btwnexch  29675  btwndiff  29677  ifscgr  29694  lineid  29733  btwnconn1lem7  29743  btwnconn1lem8  29744  btwnconn1lem9  29745  btwnconn1lem12  29748  midofsegid  29754  brsegle2  29759  btwnoutside  29775  outsideoftr  29779  cnres2  30259  heibor  30317  mzpmfp  30679  mzpmfpOLD  30680  mzpsubst  30681  pellexlem5  30769  pell14qrexpclnn0  30802  pellfundex  30822  qirropth  30844  monotuz  30877  expmordi  30883  congmul  30905  congsub  30908  mzpcong  30910  fzmaxdif  30919  jm2.15nn0  30945  idomsubgmo  31155  fourierdlem42  31931  fourierdlem48  31937  fourierdlem80  31969  lidldomn1  32727  rngccatidOLD  32797  ringccatidOLD  32860  coe1sclmulval  32985  lsmsat  34733  lkrlsp  34827  lkrlsp2  34828  lkrlsp3  34829  lshpkrlem6  34840  latm4  34958  omlspjN  34986  hlatj4  35098  4noncolr3  35177  4noncolr2  35178  4noncolr1  35179  3dimlem3a  35184  3dimlem4a  35187  3dimlem4  35188  3dimlem4OLDN  35189  1cvratex  35197  hlatexch4  35205  3atlem4  35210  atcvrlln2  35243  atcvrlln  35244  llnmlplnN  35263  lplnnlelln  35267  lvoli2  35305  lvolnlelln  35308  lvolnlelpln  35309  4atlem11b  35332  4atlem12b  35335  2lplnj  35344  dalemzeo  35357  dath2  35461  lncvrat  35506  cdlemb  35518  elpaddri  35526  padd4N  35564  llnmod2i2  35587  llnexchb2  35593  dalawlem1  35595  dalawlem2  35596  osumcllem6N  35685  pexmidlem3N  35696  pexmidlem4N  35697  lhp2lt  35725  lhp2at0  35756  lhp2atne  35758  lhp2at0ne  35760  lhpmod2i2  35762  lhpmod6i1  35763  lhpat  35767  lhpat3  35770  4atexlemex6  35798  ltrncoval  35869  ltrncnv  35870  ltrnnidn  35899  cdlemd7  35929  cdleme0b  35937  cdleme0c  35938  cdleme0fN  35943  cdleme0ex1N  35948  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme7  35974  cdleme11a  35985  cdleme17c  36013  cdleme22gb  36019  cdlemeda  36023  cdleme20k  36045  cdleme21a  36051  cdleme21at  36054  cdleme21d  36056  cdleme22f2  36073  cdleme22g  36074  cdleme24  36078  cdleme28  36099  cdlemefrs29cpre1  36124  cdlemefr29exN  36128  cdlemefr32sn2aw  36130  cdleme32fva  36163  cdleme32fva1  36164  cdleme35a  36174  cdleme42c  36198  cdleme42e  36205  cdleme42f  36206  cdleme42g  36207  cdleme42h  36208  cdleme43bN  36216  cdleme46f2g2  36219  cdleme17d2  36221  cdleme4gfv  36233  cdlemeg46c  36239  cdlemeg46nlpq  36243  cdlemeg46gfre  36258  cdlemeg49lebilem  36265  cdleme50trn1  36275  cdleme50trn2  36277  cdleme50ltrn  36283  cdleme  36286  cdlemf1  36287  cdlemf  36289  trlord  36295  ltrniotavalbN  36310  cdlemg1cex  36314  cdlemg2dN  36316  cdlemg2ce  36318  cdlemg2fvlem  36320  cdlemg2idN  36322  cdlemg2kq  36328  cdlemg2l  36329  cdlemg7fvN  36350  cdlemg7aN  36351  cdlemg8a  36353  cdlemg11aq  36364  cdlemg12d  36372  cdlemg13a  36377  cdlemg13  36378  cdlemg14f  36379  cdlemg14g  36380  cdlemg17b  36388  cdlemg27a  36418  cdlemg31b0N  36420  cdlemg31a  36423  cdlemg31b  36424  cdlemg31c  36425  ltrnco  36445  trlcoabs2N  36448  trlcocnvat  36450  trlconid  36451  trlcolem  36452  cdlemg42  36455  cdlemg43  36456  cdlemg47a  36460  cdlemg46  36461  cdlemg47  36462  tendoeq1  36490  tendocoval  36492  tendoco2  36494  tendoplco2  36505  tendopltp  36506  cdlemh1  36541  cdlemh2  36542  cdlemi1  36544  cdlemi  36546  cdlemk1  36557  cdlemk2  36558  cdlemk3  36559  cdlemk4  36560  cdlemk8  36564  cdlemk9  36565  cdlemk9bN  36566  cdlemk31  36622  cdlemk28-3  36634  cdlemk19xlem  36668  cdlemk39u  36694  cdlemk19u  36696  cdlemk56w  36699  cdlemn7  36930  cdlemn8  36931  cdlemn9  36932  dihordlem6  36940  dihordlem7  36941  dihordlem7b  36942  dihord1  36945  dihord2a  36946  dihord11c  36951  dihord2pre  36952  dihord2pre2  36953  dihlsscpre  36961  dihord4  36985  dihord6b  36987  dihmeetlem2N  37026  dihglbcpreN  37027  dihmeetcN  37029  dihmeetbclemN  37031  dihmeetlem3N  37032  dihmeetlem9N  37042  dihmeetlem13N  37046  dihmeetlem20N  37053  mapdpglem24  37431  mapdpglem32  37432  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  mapdh9aOLDN  37518  hdmap14lem6  37603

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 185  df-an 371  df-3an 975