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  7190  f1resrcmplf1d  7280  f1oiso2  7361  fnsuppres  8196  frrlem4  8295  omeulem2  8577  uniinqs  8804  unxpdomlem3  9228  sup0  9437  fin23lem11  10319  reclem3pr  11052  dedekind  11391  addlid  11411  subaddmulsub  11695  dmdcan  11943  nnadddir  12310  xaddass2  13294  xlt2add  13304  xadddi2  13341  expaddzlem  14161  expaddz  14162  expmulz  14164  expdiv  14169  expmordi  14223  pfxeq  14757  ccatopth2  14778  relexpaddnn  15114  o1add  15691  o1mul  15692  o1sub  15693  ntrivcvgmul  15982  prmexpb  16803  pcpremul  16928  pcdiv  16937  pcqmul  16938  pcqdiv  16942  4sqlem12  17041  f1ocpbllem  17603  ercpbl  17628  erlecpbl  17629  latjlej12  18536  latmlem12  18552  latj4  18570  gsumsgrpccat  18930  symgsssg  19568  symgfisg  19569  mndodcong  19643  cmn4  19902  ablsub4  19911  abladdsub4  19912  lsm4  19961  abvdom  20970  abvtrivd  20972  orngmul  21005  lspsnvs  21275  lspsneu  21284  lspfixed  21289  lspexch  21290  lsmcv  21302  lspsolvlem  21303  mvrf1  22172  coe1sclmulfv  22481  m1detdiag  22791  cnprest  23483  isreg2  23571  elptr  23767  hausflimlem  24173  trcfilu  24487  ssblps  24616  ssbl  24617  prdsxmslem2  24723  tgqioo  24994  metnrm  25057  bndth  25154  ncvspi  25352  cph2ass  25409  iscau3  25474  ovolunlem2  25694  dvres2  26108  dvfsumlem2  26223  dvfsum2  26230  deg1tm  26313  plyadd  26411  plymul  26412  coeeu  26419  coemullem  26444  aalioulem4  26535  cxplea  26898  cxple2  26899  cxplt2  26900  cxple2a  26901  cxpcn3lem  26949  angcan  27004  ang180lem5  27015  divsqrtsumlem  27181  logexprlim  27426  dchrvmasumlema  27701  dchrisum0lema  27715  logdivsum  27734  log2sumbnd  27745  padicabv  27831  nolesgn2ores  27873  nogesgn1o  27874  nogesgn1ores  27875  nolt02o  27896  nogt01o  27897  nosupinfsep  27933  noetalem1  27942  noeta2  27991  cutbdaylt  28028  expsgt0  28667  bdayfinbndlem1  28697  tghilberti2  28948  brbtwn2  29292  axcontlem4  29354  axcontlem8  29358  clwlkl1loop  30169  chscllem4  32029  mdslmd4i  32722  nexple  33214  measxun2  34632  measun  34633  mbfmco2  34687  probun  34841  satfv1fvfmla1  35936  wsuclem  36336  cgrcomim  36502  cgrcoml  36509  cgrcomr  36510  cgrdegen  36517  btwnintr  36532  btwnexch3  36533  btwnouttr  36537  btwnexch  36538  btwndiff  36540  ifscgr  36557  lineid  36596  btwnconn1lem7  36606  btwnconn1lem8  36607  btwnconn1lem9  36608  btwnconn1lem12  36611  midofsegid  36617  brsegle2  36622  btwnoutside  36638  outsideoftr  36642  ttcmin  37048  cnres2  38455  heibor  38513  lsmsat  39823  lkrlsp  39917  lkrlsp2  39918  lkrlsp3  39919  lshpkrlem6  39930  latm4  40048  omlspjN  40076  hlatj4  40189  4noncolr3  40268  4noncolr2  40269  4noncolr1  40270  3dimlem3a  40275  3dimlem4a  40278  3dimlem4  40279  3dimlem4OLDN  40280  1cvratex  40288  hlatexch4  40296  3atlem4  40301  atcvrlln2  40334  atcvrlln  40335  llnmlplnN  40354  lplnnlelln  40358  lvoli2  40396  lvolnlelln  40399  lvolnlelpln  40400  4atlem11b  40423  4atlem12b  40426  2lplnj  40435  dalemzeo  40448  dath2  40552  lncvrat  40597  cdlemb  40609  elpaddri  40617  padd4N  40655  llnmod2i2  40678  llnexchb2  40684  dalawlem1  40686  dalawlem2  40687  osumcllem6N  40776  pexmidlem3N  40787  pexmidlem4N  40788  lhp2lt  40816  lhp2at0  40847  lhp2atne  40849  lhp2at0ne  40851  lhpmod2i2  40853  lhpmod6i1  40854  lhpat  40858  lhpat3  40861  4atexlemex6  40889  ltrncoval  40960  ltrncnv  40961  ltrnnidn  40989  cdlemd7  41019  cdleme0b  41027  cdleme0c  41028  cdleme0fN  41033  cdleme0ex1N  41038  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme11a  41075  cdleme17c  41103  cdleme22gb  41109  cdlemeda  41113  cdleme20k  41134  cdleme21a  41140  cdleme21at  41143  cdleme21d  41145  cdleme22f2  41162  cdleme22g  41163  cdleme24  41167  cdleme28  41188  cdlemefrs29cpre1  41213  cdlemefr29exN  41217  cdlemefr32sn2aw  41219  cdleme32fva  41252  cdleme32fva1  41253  cdleme35a  41263  cdleme42c  41287  cdleme42e  41294  cdleme42f  41295  cdleme42g  41296  cdleme42h  41297  cdleme43bN  41305  cdleme46f2g2  41308  cdleme17d2  41310  cdleme4gfv  41322  cdlemeg46c  41328  cdlemeg46nlpq  41332  cdlemeg46gfre  41347  cdlemeg49lebilem  41354  cdleme50trn1  41364  cdleme50trn2  41366  cdleme50ltrn  41372  cdleme  41375  cdlemf1  41376  cdlemf  41378  trlord  41384  ltrniotavalbN  41399  cdlemg1cex  41403  cdlemg2dN  41405  cdlemg2ce  41407  cdlemg2fvlem  41409  cdlemg2idN  41411  cdlemg2kq  41417  cdlemg2l  41418  cdlemg7fvN  41439  cdlemg7aN  41440  cdlemg8a  41442  cdlemg11aq  41453  cdlemg12d  41461  cdlemg13a  41466  cdlemg13  41467  cdlemg14f  41468  cdlemg14g  41469  cdlemg17b  41477  cdlemg27a  41507  cdlemg31b0N  41509  cdlemg31a  41512  cdlemg31b  41513  cdlemg31c  41514  ltrnco  41534  trlcoabs2N  41537  trlcocnvat  41539  trlconid  41540  trlcolem  41541  cdlemg42  41544  cdlemg43  41545  cdlemg47a  41549  cdlemg46  41550  cdlemg47  41551  tendoeq1  41579  tendocoval  41581  tendoco2  41583  tendoplco2  41594  tendopltp  41595  cdlemh1  41630  cdlemh2  41631  cdlemi1  41633  cdlemi  41635  cdlemk1  41646  cdlemk2  41647  cdlemk3  41648  cdlemk4  41649  cdlemk8  41653  cdlemk9  41654  cdlemk9bN  41655  cdlemk31  41711  cdlemk28-3  41723  cdlemk19xlem  41757  cdlemk39u  41783  cdlemk19u  41785  cdlemk56w  41788  cdlemn7  42018  cdlemn8  42019  cdlemn9  42020  dihordlem6  42028  dihordlem7  42029  dihordlem7b  42030  dihord1  42033  dihord2a  42034  dihord11c  42039  dihord2pre  42040  dihord2pre2  42041  dihlsscpre  42049  dihord4  42073  dihord6b  42075  dihmeetlem2N  42114  dihglbcpreN  42115  dihmeetcN  42117  dihmeetbclemN  42119  dihmeetlem3N  42120  dihmeetlem9N  42130  dihmeetlem13N  42134  dihmeetlem20N  42141  mapdpglem24  42519  mapdpglem32  42520  baerlem3lem2  42525  baerlem5alem2  42526  baerlem5blem2  42527  mapdh9aOLDN  42605  hdmap14lem6  42688  sn-addlid  43206  mzpmfp  43519  mzpsubst  43520  pellexlem5  43601  pell14qrexpclnn0  43634  pellfundex  43654  qirropth  43676  monotuz  43709  congmul  43735  congsub  43738  mzpcong  43740  fzmaxdif  43749  jm2.15nn0  43771  idomsubgmo  43961  trclimalb2  44493  mnringmulrcld  44993  fourierdlem42  46904  fourierdlem48  46909  fourierdlem80  46941  prmdvdsfmtnof1lem1  48377  cycldlenngric  48734  gpgedgvtx1  48868  lidldomn1  49037  rngccatidALTV  49078  ringccatidALTV  49112  coe1sclmulval  49206  line2  49573  line2xlem  49574  line2x  49575  line2y  49576  itsclc0yqsol  49585  seposep  49745  iscnrm3rlem8  49766  iscnrm3llem2  49769