Theorem simp2r 1199

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp12r  1286  simp22r  1292  simp32r  1298  fsnunf  7066  f1oiso2  7232  fnsuppres  8016  frrlem4  8114  omeulem2  8423  uniinqs  8595  unxpdomlem3  9038  sup0  9234  fin23lem11  10082  reclem3pr  10814  dedekind  11147  addid2  11167  subaddmulsub  11447  dmdcan  11694  xaddass2  12993  xlt2add  13003  xadddi2  13040  expaddzlem  13835  expaddz  13836  expmulz  13838  expdiv  13843  expmordi  13894  pfxeq  14418  ccatopth2  14439  relexpaddnn  14771  o1add  15332  o1mul  15333  o1sub  15334  ntrivcvgmul  15623  prmexpb  16434  pcpremul  16553  pcdiv  16562  pcqmul  16563  pcqdiv  16567  4sqlem12  16666  f1ocpbllem  17244  ercpbl  17269  erlecpbl  17270  latjlej12  18182  latmlem12  18198  latj4  18216  gsumsgrpccat  18487  symgsssg  19084  symgfisg  19085  mndodcong  19159  cmn4  19415  ablsub4  19423  abladdsub4  19424  lsm4  19470  abvdom  20107  abvtrivd  20109  lspsnvs  20385  lspsneu  20394  lspfixed  20399  lspexch  20400  lsmcv  20412  lspsolvlem  20413  mvrf1  21203  coe1sclmulfv  21463  m1detdiag  21755  cnprest  22449  isreg2  22537  elptr  22733  hausflimlem  23139  trcfilu  23455  ssblps  23584  ssbl  23585  prdsxmslem2  23694  tgqioo  23972  metnrm  24034  bndth  24130  ncvspi  24329  cph2ass  24386  iscau3  24451  ovolunlem2  24671  dvres2  25085  dvfsumlem2  25200  dvfsum2  25207  deg1tm  25292  plyadd  25387  plymul  25388  coeeu  25395  coemullem  25420  aalioulem4  25504  cxplea  25860  cxple2  25861  cxplt2  25862  cxple2a  25863  cxpcn3lem  25909  angcan  25961  ang180lem5  25972  divsqrtsumlem  26138  logexprlim  26382  dchrvmasumlema  26657  dchrisum0lema  26671  logdivsum  26690  log2sumbnd  26701  padicabv  26787  tghilberti2  27008  brbtwn2  27282  axcontlem4  27344  axcontlem8  27348  clwlkl1loop  28160  chscllem4  30011  mdslmd4i  30704  orngmul  31511  nexple  31986  measxun2  32187  measun  32188  mbfmco2  32241  probun  32395  satfv1fvfmla1  33394  wsuclem  33828  nolesgn2ores  33884  nogesgn1o  33885  nogesgn1ores  33886  nolt02o  33907  nogt01o  33908  nosupinfsep  33944  noetalem1  33953  noeta2  33988  scutbdaylt  34021  cgrcomim  34300  cgrcoml  34307  cgrcomr  34308  cgrdegen  34315  btwnintr  34330  btwnexch3  34331  btwnouttr  34335  btwnexch  34336  btwndiff  34338  ifscgr  34355  lineid  34394  btwnconn1lem7  34404  btwnconn1lem8  34405  btwnconn1lem9  34406  btwnconn1lem12  34409  midofsegid  34415  brsegle2  34420  btwnoutside  34436  outsideoftr  34440  cnres2  35930  heibor  35988  lsmsat  37029  lkrlsp  37123  lkrlsp2  37124  lkrlsp3  37125  lshpkrlem6  37136  latm4  37254  omlspjN  37282  hlatj4  37395  4noncolr3  37474  4noncolr2  37475  4noncolr1  37476  3dimlem3a  37481  3dimlem4a  37484  3dimlem4  37485  3dimlem4OLDN  37486  1cvratex  37494  hlatexch4  37502  3atlem4  37507  atcvrlln2  37540  atcvrlln  37541  llnmlplnN  37560  lplnnlelln  37564  lvoli2  37602  lvolnlelln  37605  lvolnlelpln  37606  4atlem11b  37629  4atlem12b  37632  2lplnj  37641  dalemzeo  37654  dath2  37758  lncvrat  37803  cdlemb  37815  elpaddri  37823  padd4N  37861  llnmod2i2  37884  llnexchb2  37890  dalawlem1  37892  dalawlem2  37893  osumcllem6N  37982  pexmidlem3N  37993  pexmidlem4N  37994  lhp2lt  38022  lhp2at0  38053  lhp2atne  38055  lhp2at0ne  38057  lhpmod2i2  38059  lhpmod6i1  38060  lhpat  38064  lhpat3  38067  4atexlemex6  38095  ltrncoval  38166  ltrncnv  38167  ltrnnidn  38195  cdlemd7  38225  cdleme0b  38233  cdleme0c  38234  cdleme0fN  38239  cdleme0ex1N  38244  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme11a  38281  cdleme17c  38309  cdleme22gb  38315  cdlemeda  38319  cdleme20k  38340  cdleme21a  38346  cdleme21at  38349  cdleme21d  38351  cdleme22f2  38368  cdleme22g  38369  cdleme24  38373  cdleme28  38394  cdlemefrs29cpre1  38419  cdlemefr29exN  38423  cdlemefr32sn2aw  38425  cdleme32fva  38458  cdleme32fva1  38459  cdleme35a  38469  cdleme42c  38493  cdleme42e  38500  cdleme42f  38501  cdleme42g  38502  cdleme42h  38503  cdleme43bN  38511  cdleme46f2g2  38514  cdleme17d2  38516  cdleme4gfv  38528  cdlemeg46c  38534  cdlemeg46nlpq  38538  cdlemeg46gfre  38553  cdlemeg49lebilem  38560  cdleme50trn1  38570  cdleme50trn2  38572  cdleme50ltrn  38578  cdleme  38581  cdlemf1  38582  cdlemf  38584  trlord  38590  ltrniotavalbN  38605  cdlemg1cex  38609  cdlemg2dN  38611  cdlemg2ce  38613  cdlemg2fvlem  38615  cdlemg2idN  38617  cdlemg2kq  38623  cdlemg2l  38624  cdlemg7fvN  38645  cdlemg7aN  38646  cdlemg8a  38648  cdlemg11aq  38659  cdlemg12d  38667  cdlemg13a  38672  cdlemg13  38673  cdlemg14f  38674  cdlemg14g  38675  cdlemg17b  38683  cdlemg27a  38713  cdlemg31b0N  38715  cdlemg31a  38718  cdlemg31b  38719  cdlemg31c  38720  ltrnco  38740  trlcoabs2N  38743  trlcocnvat  38745  trlconid  38746  trlcolem  38747  cdlemg42  38750  cdlemg43  38751  cdlemg47a  38755  cdlemg46  38756  cdlemg47  38757  tendoeq1  38785  tendocoval  38787  tendoco2  38789  tendoplco2  38800  tendopltp  38801  cdlemh1  38836  cdlemh2  38837  cdlemi1  38839  cdlemi  38841  cdlemk1  38852  cdlemk2  38853  cdlemk3  38854  cdlemk4  38855  cdlemk8  38859  cdlemk9  38860  cdlemk9bN  38861  cdlemk31  38917  cdlemk28-3  38929  cdlemk19xlem  38963  cdlemk39u  38989  cdlemk19u  38991  cdlemk56w  38994  cdlemn7  39224  cdlemn8  39225  cdlemn9  39226  dihordlem6  39234  dihordlem7  39235  dihordlem7b  39236  dihord1  39239  dihord2a  39240  dihord11c  39245  dihord2pre  39246  dihord2pre2  39247  dihlsscpre  39255  dihord4  39279  dihord6b  39281  dihmeetlem2N  39320  dihglbcpreN  39321  dihmeetcN  39323  dihmeetbclemN  39325  dihmeetlem3N  39326  dihmeetlem9N  39336  dihmeetlem13N  39340  dihmeetlem20N  39347  mapdpglem24  39725  mapdpglem32  39726  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  mapdh9aOLDN  39811  hdmap14lem6  39894  nnadddir  40307  sn-addid2  40394  mzpmfp  40576  mzpsubst  40577  pellexlem5  40662  pell14qrexpclnn0  40695  pellfundex  40715  qirropth  40737  monotuz  40770  congmul  40796  congsub  40799  mzpcong  40801  fzmaxdif  40810  jm2.15nn0  40832  idomsubgmo  41030  trclimalb2  41341  mnringmulrcld  41853  fourierdlem42  43697  fourierdlem48  43702  fourierdlem80  43734  prmdvdsfmtnof1lem1  45047  lidldomn1  45490  rngccatidALTV  45558  ringccatidALTV  45621  coe1sclmulval  45737  line2  46109  line2xlem  46110  line2x  46111  line2y  46112  itsclc0yqsol  46121  seposep  46230  iscnrm3rlem8  46252  iscnrm3llem2  46255