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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp12r  1286  simp22r  1292  simp32r  1298  fsnunf  7204  f1oiso2  7371  fnsuppres  8214  frrlem4  8312  omeulem2  8619  uniinqs  8835  unxpdomlem3  9285  sup0  9503  fin23lem11  10354  reclem3pr  11086  dedekind  11421  addlid  11441  subaddmulsub  11723  dmdcan  11974  xaddass2  13288  xlt2add  13298  xadddi2  13335  expaddzlem  14142  expaddz  14143  expmulz  14145  expdiv  14150  expmordi  14203  pfxeq  14730  ccatopth2  14751  relexpaddnn  15086  o1add  15646  o1mul  15647  o1sub  15648  ntrivcvgmul  15934  prmexpb  16752  pcpremul  16876  pcdiv  16885  pcqmul  16886  pcqdiv  16890  4sqlem12  16989  f1ocpbllem  17570  ercpbl  17595  erlecpbl  17596  latjlej12  18512  latmlem12  18528  latj4  18546  gsumsgrpccat  18865  symgsssg  19499  symgfisg  19500  mndodcong  19574  cmn4  19833  ablsub4  19842  abladdsub4  19843  lsm4  19892  abvdom  20847  abvtrivd  20849  lspsnvs  21133  lspsneu  21142  lspfixed  21147  lspexch  21148  lsmcv  21160  lspsolvlem  21161  mvrf1  22023  coe1sclmulfv  22301  m1detdiag  22618  cnprest  23312  isreg2  23400  elptr  23596  hausflimlem  24002  trcfilu  24318  ssblps  24447  ssbl  24448  prdsxmslem2  24557  tgqioo  24835  metnrm  24897  bndth  25003  ncvspi  25203  cph2ass  25260  iscau3  25325  ovolunlem2  25546  dvres2  25961  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsum2  26089  deg1tm  26172  plyadd  26270  plymul  26271  coeeu  26278  coemullem  26303  aalioulem4  26391  cxplea  26752  cxple2  26753  cxplt2  26754  cxple2a  26755  cxpcn3lem  26804  angcan  26859  ang180lem5  26870  divsqrtsumlem  27037  logexprlim  27283  dchrvmasumlema  27558  dchrisum0lema  27572  logdivsum  27591  log2sumbnd  27602  padicabv  27688  nolesgn2ores  27731  nogesgn1o  27732  nogesgn1ores  27733  nolt02o  27754  nogt01o  27755  nosupinfsep  27791  noetalem1  27800  noeta2  27843  scutbdaylt  27877  expsgt0  28429  tghilberti2  28660  brbtwn2  28934  axcontlem4  28996  axcontlem8  29000  clwlkl1loop  29815  chscllem4  31668  mdslmd4i  32361  orngmul  33312  nexple  33989  measxun2  34190  measun  34191  mbfmco2  34246  probun  34400  satfv1fvfmla1  35407  wsuclem  35806  cgrcomim  35970  cgrcoml  35977  cgrcomr  35978  cgrdegen  35985  btwnintr  36000  btwnexch3  36001  btwnouttr  36005  btwnexch  36006  btwndiff  36008  ifscgr  36025  lineid  36064  btwnconn1lem7  36074  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem12  36079  midofsegid  36085  brsegle2  36090  btwnoutside  36106  outsideoftr  36110  cnres2  37749  heibor  37807  lsmsat  38989  lkrlsp  39083  lkrlsp2  39084  lkrlsp3  39085  lshpkrlem6  39096  latm4  39214  omlspjN  39242  hlatj4  39355  4noncolr3  39435  4noncolr2  39436  4noncolr1  39437  3dimlem3a  39442  3dimlem4a  39445  3dimlem4  39446  3dimlem4OLDN  39447  1cvratex  39455  hlatexch4  39463  3atlem4  39468  atcvrlln2  39501  atcvrlln  39502  llnmlplnN  39521  lplnnlelln  39525  lvoli2  39563  lvolnlelln  39566  lvolnlelpln  39567  4atlem11b  39590  4atlem12b  39593  2lplnj  39602  dalemzeo  39615  dath2  39719  lncvrat  39764  cdlemb  39776  elpaddri  39784  padd4N  39822  llnmod2i2  39845  llnexchb2  39851  dalawlem1  39853  dalawlem2  39854  osumcllem6N  39943  pexmidlem3N  39954  pexmidlem4N  39955  lhp2lt  39983  lhp2at0  40014  lhp2atne  40016  lhp2at0ne  40018  lhpmod2i2  40020  lhpmod6i1  40021  lhpat  40025  lhpat3  40028  4atexlemex6  40056  ltrncoval  40127  ltrncnv  40128  ltrnnidn  40156  cdlemd7  40186  cdleme0b  40194  cdleme0c  40195  cdleme0fN  40200  cdleme0ex1N  40205  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme11a  40242  cdleme17c  40270  cdleme22gb  40276  cdlemeda  40280  cdleme20k  40301  cdleme21a  40307  cdleme21at  40310  cdleme21d  40312  cdleme22f2  40329  cdleme22g  40330  cdleme24  40334  cdleme28  40355  cdlemefrs29cpre1  40380  cdlemefr29exN  40384  cdlemefr32sn2aw  40386  cdleme32fva  40419  cdleme32fva1  40420  cdleme35a  40430  cdleme42c  40454  cdleme42e  40461  cdleme42f  40462  cdleme42g  40463  cdleme42h  40464  cdleme43bN  40472  cdleme46f2g2  40475  cdleme17d2  40477  cdleme4gfv  40489  cdlemeg46c  40495  cdlemeg46nlpq  40499  cdlemeg46gfre  40514  cdlemeg49lebilem  40521  cdleme50trn1  40531  cdleme50trn2  40533  cdleme50ltrn  40539  cdleme  40542  cdlemf1  40543  cdlemf  40545  trlord  40551  ltrniotavalbN  40566  cdlemg1cex  40570  cdlemg2dN  40572  cdlemg2ce  40574  cdlemg2fvlem  40576  cdlemg2idN  40578  cdlemg2kq  40584  cdlemg2l  40585  cdlemg7fvN  40606  cdlemg7aN  40607  cdlemg8a  40609  cdlemg11aq  40620  cdlemg12d  40628  cdlemg13a  40633  cdlemg13  40634  cdlemg14f  40635  cdlemg14g  40636  cdlemg17b  40644  cdlemg27a  40674  cdlemg31b0N  40676  cdlemg31a  40679  cdlemg31b  40680  cdlemg31c  40681  ltrnco  40701  trlcoabs2N  40704  trlcocnvat  40706  trlconid  40707  trlcolem  40708  cdlemg42  40711  cdlemg43  40712  cdlemg47a  40716  cdlemg46  40717  cdlemg47  40718  tendoeq1  40746  tendocoval  40748  tendoco2  40750  tendoplco2  40761  tendopltp  40762  cdlemh1  40797  cdlemh2  40798  cdlemi1  40800  cdlemi  40802  cdlemk1  40813  cdlemk2  40814  cdlemk3  40815  cdlemk4  40816  cdlemk8  40820  cdlemk9  40821  cdlemk9bN  40822  cdlemk31  40878  cdlemk28-3  40890  cdlemk19xlem  40924  cdlemk39u  40950  cdlemk19u  40952  cdlemk56w  40955  cdlemn7  41185  cdlemn8  41186  cdlemn9  41187  dihordlem6  41195  dihordlem7  41196  dihordlem7b  41197  dihord1  41200  dihord2a  41201  dihord11c  41206  dihord2pre  41207  dihord2pre2  41208  dihlsscpre  41216  dihord4  41240  dihord6b  41242  dihmeetlem2N  41281  dihglbcpreN  41282  dihmeetcN  41284  dihmeetbclemN  41286  dihmeetlem3N  41287  dihmeetlem9N  41297  dihmeetlem13N  41301  dihmeetlem20N  41308  mapdpglem24  41686  mapdpglem32  41687  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  mapdh9aOLDN  41772  hdmap14lem6  41855  nnadddir  42283  sn-addlid  42410  mzpmfp  42734  mzpsubst  42735  pellexlem5  42820  pell14qrexpclnn0  42853  pellfundex  42873  qirropth  42895  monotuz  42929  congmul  42955  congsub  42958  mzpcong  42960  fzmaxdif  42969  jm2.15nn0  42991  idomsubgmo  43181  trclimalb2  43715  mnringmulrcld  44223  fourierdlem42  46104  fourierdlem48  46109  fourierdlem80  46141  prmdvdsfmtnof1lem1  47508  gpgedgvtx1  47954  lidldomn1  48074  rngccatidALTV  48115  ringccatidALTV  48149  coe1sclmulval  48230  line2  48601  line2xlem  48602  line2x  48603  line2y  48604  itsclc0yqsol  48613  seposep  48721  iscnrm3rlem8  48743  iscnrm3llem2  48746