Theorem simp2r 1219

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp12r  1306  simp22r  1312  simp32r  1318  fsnunf  7182  f1resrcmplf1d  7271  f1oiso2  7352  fnsuppres  8192  frrlem4  8291  omeulem2  8575  uniinqs  8802  unxpdomlem3  9233  sup0  9443  fin23lem11  10376  reclem3pr  11115  dedekind  11454  addlid  11474  subaddmulsub  11760  dmdcan  12008  nnadddir  12375  xaddass2  13361  xlt2add  13371  xadddi2  13408  expaddzlem  14228  expaddz  14229  expmulz  14231  expdiv  14236  expmordi  14290  pfxeq  14825  ccatopth2  14846  relexpaddnn  15184  o1add  15761  o1mul  15762  o1sub  15763  ntrivcvgmul  16051  prmexpb  16875  pcpremul  17001  pcdiv  17010  pcqmul  17011  pcqdiv  17015  4sqlem12  17114  f1ocpbllem  17676  ercpbl  17701  erlecpbl  17702  latjlej12  18609  latmlem12  18625  latj4  18643  gsumsgrpccat  19016  symgsssg  19661  symgfisg  19662  mndodcong  19736  cmn4  19995  ablsub4  20004  abladdsub4  20005  lsm4  20054  abvdom  21067  abvtrivd  21069  orngmul  21102  lspsnvs  21372  lspsneu  21381  lspfixed  21386  lspexch  21387  lsmcv  21399  lspsolvlem  21400  mvrf1  22273  coe1sclmulfv  22582  m1detdiag  22892  cnprest  23587  isreg2  23675  elptr  23872  hausflimlem  24278  trcfilu  24592  ssblps  24721  ssbl  24722  prdsxmslem2  24828  tgqioo  25099  metnrm  25162  bndth  25259  ncvspi  25457  cph2ass  25514  iscau3  25579  ovolunlem2  25799  dvres2  26212  dvfsumlem2  26327  dvfsum2  26334  deg1tm  26417  plyadd  26516  plymul  26517  coeeu  26524  coemullem  26549  aalioulem4  26644  cxplea  27006  cxple2  27007  cxplt2  27008  cxple2a  27009  cxpcn3lem  27057  angcan  27112  ang180lem5  27123  divsqrtsumlem  27289  logexprlim  27534  dchrvmasumlema  27809  dchrisum0lema  27823  logdivsum  27842  log2sumbnd  27853  padicabv  27939  nolesgn2ores  28011  nogesgn1o  28012  nogesgn1ores  28013  nolt02o  28034  nogt01o  28035  nosupinfsep  28071  noetalem1  28080  noeta2  28129  cutbdaylt  28166  expsgt0  28805  bdayfinbndlem1  28835  tghilberti2  29088  brbtwn2  29465  axcontlem4  29527  axcontlem8  29531  clwlkl1loop  30352  umgr2cycllem  30728  chscllem4  32224  mdslmd4i  32917  nexple  33406  measxun2  34825  measun  34826  mbfmco2  34880  probun  35034  satfv1fvfmla1  36157  wsuclem  36557  cgrcomim  36724  cgrcoml  36731  cgrcomr  36732  cgrdegen  36739  btwnintr  36754  btwnexch3  36755  btwnouttr  36759  btwnexch  36760  btwndiff  36762  ifscgr  36779  lineid  36818  btwnconn1lem7  36828  btwnconn1lem8  36829  btwnconn1lem9  36830  btwnconn1lem12  36833  midofsegid  36839  brsegle2  36844  btwnoutside  36860  outsideoftr  36864  ttcmin  37254  cnres2  38665  heibor  38723  lsmsat  40033  lkrlsp  40127  lkrlsp2  40128  lkrlsp3  40129  lshpkrlem6  40140  latm4  40258  omlspjN  40286  hlatj4  40399  4noncolr3  40478  4noncolr2  40479  4noncolr1  40480  3dimlem3a  40485  3dimlem4a  40488  3dimlem4  40489  3dimlem4OLDN  40490  1cvratex  40498  hlatexch4  40506  3atlem4  40511  atcvrlln2  40544  atcvrlln  40545  llnmlplnN  40564  lplnnlelln  40568  lvoli2  40606  lvolnlelln  40609  lvolnlelpln  40610  4atlem11b  40633  4atlem12b  40636  2lplnj  40645  dalemzeo  40658  dath2  40762  lncvrat  40807  cdlemb  40819  elpaddri  40827  padd4N  40865  llnmod2i2  40888  llnexchb2  40894  dalawlem1  40896  dalawlem2  40897  osumcllem6N  40986  pexmidlem3N  40997  pexmidlem4N  40998  lhp2lt  41026  lhp2at0  41057  lhp2atne  41059  lhp2at0ne  41061  lhpmod2i2  41063  lhpmod6i1  41064  lhpat  41068  lhpat3  41071  4atexlemex6  41099  ltrncoval  41170  ltrncnv  41171  ltrnnidn  41199  cdlemd7  41229  cdleme0b  41237  cdleme0c  41238  cdleme0fN  41243  cdleme0ex1N  41248  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme11a  41285  cdleme17c  41313  cdleme22gb  41319  cdlemeda  41323  cdleme20k  41344  cdleme21a  41350  cdleme21at  41353  cdleme21d  41355  cdleme22f2  41372  cdleme22g  41373  cdleme24  41377  cdleme28  41398  cdlemefrs29cpre1  41423  cdlemefr29exN  41427  cdlemefr32sn2aw  41429  cdleme32fva  41462  cdleme32fva1  41463  cdleme35a  41473  cdleme42c  41497  cdleme42e  41504  cdleme42f  41505  cdleme42g  41506  cdleme42h  41507  cdleme43bN  41515  cdleme46f2g2  41518  cdleme17d2  41520  cdleme4gfv  41532  cdlemeg46c  41538  cdlemeg46nlpq  41542  cdlemeg46gfre  41557  cdlemeg49lebilem  41564  cdleme50trn1  41574  cdleme50trn2  41576  cdleme50ltrn  41582  cdleme  41585  cdlemf1  41586  cdlemf  41588  trlord  41594  ltrniotavalbN  41609  cdlemg1cex  41613  cdlemg2dN  41615  cdlemg2ce  41617  cdlemg2fvlem  41619  cdlemg2idN  41621  cdlemg2kq  41627  cdlemg2l  41628  cdlemg7fvN  41649  cdlemg7aN  41650  cdlemg8a  41652  cdlemg11aq  41663  cdlemg12d  41671  cdlemg13a  41676  cdlemg13  41677  cdlemg14f  41678  cdlemg14g  41679  cdlemg17b  41687  cdlemg27a  41717  cdlemg31b0N  41719  cdlemg31a  41722  cdlemg31b  41723  cdlemg31c  41724  ltrnco  41744  trlcoabs2N  41747  trlcocnvat  41749  trlconid  41750  trlcolem  41751  cdlemg42  41754  cdlemg43  41755  cdlemg47a  41759  cdlemg46  41760  cdlemg47  41761  tendoeq1  41789  tendocoval  41791  tendoco2  41793  tendoplco2  41804  tendopltp  41805  cdlemh1  41840  cdlemh2  41841  cdlemi1  41843  cdlemi  41845  cdlemk1  41856  cdlemk2  41857  cdlemk3  41858  cdlemk4  41859  cdlemk8  41863  cdlemk9  41864  cdlemk9bN  41865  cdlemk31  41921  cdlemk28-3  41933  cdlemk19xlem  41967  cdlemk39u  41993  cdlemk19u  41995  cdlemk56w  41998  cdlemn7  42228  cdlemn8  42229  cdlemn9  42230  dihordlem6  42238  dihordlem7  42239  dihordlem7b  42240  dihord1  42243  dihord2a  42244  dihord11c  42249  dihord2pre  42250  dihord2pre2  42251  dihlsscpre  42259  dihord4  42283  dihord6b  42285  dihmeetlem2N  42324  dihglbcpreN  42325  dihmeetcN  42327  dihmeetbclemN  42329  dihmeetlem3N  42330  dihmeetlem9N  42340  dihmeetlem13N  42344  dihmeetlem20N  42351  mapdpglem24  42729  mapdpglem32  42730  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  mapdh9aOLDN  42815  hdmap14lem6  42898  sn-addlid  43423  mzpmfp  43711  mzpsubst  43712  pellexlem5  43793  pell14qrexpclnn0  43826  pellfundex  43846  qirropth  43868  monotuz  43901  congmul  43927  congsub  43930  mzpcong  43932  fzmaxdif  43941  jm2.15nn0  43963  idomsubgmo  44153  trclimalb2  44685  mnringmulrcld  45185  fourierdlem42  47103  fourierdlem48  47108  fourierdlem80  47140  prmdvdsfmtnof1lem1  48613  cycldlenngric  48970  gpgedgvtx1  49104  lidldomn1  49272  rngccatidALTV  49313  ringccatidALTV  49347  coe1sclmulval  49441  line2  49808  line2xlem  49809  line2x  49810  line2y  49811  itsclc0yqsol  49820  seposep  49978  iscnrm3rlem8  49999  iscnrm3llem2  50002