Theorem simp2r 1198

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 1132	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simp12r  1285  simp22r  1291  simp32r  1297  fsnunf  7039  f1oiso2  7203  fnsuppres  7978  frrlem4  8076  omeulem2  8376  uniinqs  8544  unxpdomlem3  8958  sup0  9155  fin23lem11  10004  reclem3pr  10736  dedekind  11068  addid2  11088  subaddmulsub  11368  dmdcan  11615  xaddass2  12913  xlt2add  12923  xadddi2  12960  expaddzlem  13754  expaddz  13755  expmulz  13757  expdiv  13762  expmordi  13813  pfxeq  14337  ccatopth2  14358  relexpaddnn  14690  o1add  15251  o1mul  15252  o1sub  15253  ntrivcvgmul  15542  prmexpb  16353  pcpremul  16472  pcdiv  16481  pcqmul  16482  pcqdiv  16486  4sqlem12  16585  f1ocpbllem  17152  ercpbl  17177  erlecpbl  17178  latjlej12  18088  latmlem12  18104  latj4  18122  gsumsgrpccat  18393  symgsssg  18990  symgfisg  18991  mndodcong  19065  cmn4  19321  ablsub4  19329  abladdsub4  19330  lsm4  19376  abvdom  20013  abvtrivd  20015  lspsnvs  20291  lspsneu  20300  lspfixed  20305  lspexch  20306  lsmcv  20318  lspsolvlem  20319  mvrf1  21104  coe1sclmulfv  21364  m1detdiag  21654  cnprest  22348  isreg2  22436  elptr  22632  hausflimlem  23038  trcfilu  23354  ssblps  23483  ssbl  23484  prdsxmslem2  23591  tgqioo  23869  metnrm  23931  bndth  24027  ncvspi  24225  cph2ass  24282  iscau3  24347  ovolunlem2  24567  dvres2  24981  dvfsumlem2  25096  dvfsum2  25103  deg1tm  25188  plyadd  25283  plymul  25284  coeeu  25291  coemullem  25316  aalioulem4  25400  cxplea  25756  cxple2  25757  cxplt2  25758  cxple2a  25759  cxpcn3lem  25805  angcan  25857  ang180lem5  25868  divsqrtsumlem  26034  logexprlim  26278  dchrvmasumlema  26553  dchrisum0lema  26567  logdivsum  26586  log2sumbnd  26597  padicabv  26683  tghilberti2  26903  brbtwn2  27176  axcontlem4  27238  axcontlem8  27242  clwlkl1loop  28052  chscllem4  29903  mdslmd4i  30596  orngmul  31404  nexple  31877  measxun2  32078  measun  32079  mbfmco2  32132  probun  32286  satfv1fvfmla1  33285  wsuclem  33746  nolesgn2ores  33802  nogesgn1o  33803  nogesgn1ores  33804  nolt02o  33825  nogt01o  33826  nosupinfsep  33862  noetalem1  33871  noeta2  33906  scutbdaylt  33939  cgrcomim  34218  cgrcoml  34225  cgrcomr  34226  cgrdegen  34233  btwnintr  34248  btwnexch3  34249  btwnouttr  34253  btwnexch  34254  btwndiff  34256  ifscgr  34273  lineid  34312  btwnconn1lem7  34322  btwnconn1lem8  34323  btwnconn1lem9  34324  btwnconn1lem12  34327  midofsegid  34333  brsegle2  34338  btwnoutside  34354  outsideoftr  34358  cnres2  35848  heibor  35906  lsmsat  36949  lkrlsp  37043  lkrlsp2  37044  lkrlsp3  37045  lshpkrlem6  37056  latm4  37174  omlspjN  37202  hlatj4  37315  4noncolr3  37394  4noncolr2  37395  4noncolr1  37396  3dimlem3a  37401  3dimlem4a  37404  3dimlem4  37405  3dimlem4OLDN  37406  1cvratex  37414  hlatexch4  37422  3atlem4  37427  atcvrlln2  37460  atcvrlln  37461  llnmlplnN  37480  lplnnlelln  37484  lvoli2  37522  lvolnlelln  37525  lvolnlelpln  37526  4atlem11b  37549  4atlem12b  37552  2lplnj  37561  dalemzeo  37574  dath2  37678  lncvrat  37723  cdlemb  37735  elpaddri  37743  padd4N  37781  llnmod2i2  37804  llnexchb2  37810  dalawlem1  37812  dalawlem2  37813  osumcllem6N  37902  pexmidlem3N  37913  pexmidlem4N  37914  lhp2lt  37942  lhp2at0  37973  lhp2atne  37975  lhp2at0ne  37977  lhpmod2i2  37979  lhpmod6i1  37980  lhpat  37984  lhpat3  37987  4atexlemex6  38015  ltrncoval  38086  ltrncnv  38087  ltrnnidn  38115  cdlemd7  38145  cdleme0b  38153  cdleme0c  38154  cdleme0fN  38159  cdleme0ex1N  38164  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme11a  38201  cdleme17c  38229  cdleme22gb  38235  cdlemeda  38239  cdleme20k  38260  cdleme21a  38266  cdleme21at  38269  cdleme21d  38271  cdleme22f2  38288  cdleme22g  38289  cdleme24  38293  cdleme28  38314  cdlemefrs29cpre1  38339  cdlemefr29exN  38343  cdlemefr32sn2aw  38345  cdleme32fva  38378  cdleme32fva1  38379  cdleme35a  38389  cdleme42c  38413  cdleme42e  38420  cdleme42f  38421  cdleme42g  38422  cdleme42h  38423  cdleme43bN  38431  cdleme46f2g2  38434  cdleme17d2  38436  cdleme4gfv  38448  cdlemeg46c  38454  cdlemeg46nlpq  38458  cdlemeg46gfre  38473  cdlemeg49lebilem  38480  cdleme50trn1  38490  cdleme50trn2  38492  cdleme50ltrn  38498  cdleme  38501  cdlemf1  38502  cdlemf  38504  trlord  38510  ltrniotavalbN  38525  cdlemg1cex  38529  cdlemg2dN  38531  cdlemg2ce  38533  cdlemg2fvlem  38535  cdlemg2idN  38537  cdlemg2kq  38543  cdlemg2l  38544  cdlemg7fvN  38565  cdlemg7aN  38566  cdlemg8a  38568  cdlemg11aq  38579  cdlemg12d  38587  cdlemg13a  38592  cdlemg13  38593  cdlemg14f  38594  cdlemg14g  38595  cdlemg17b  38603  cdlemg27a  38633  cdlemg31b0N  38635  cdlemg31a  38638  cdlemg31b  38639  cdlemg31c  38640  ltrnco  38660  trlcoabs2N  38663  trlcocnvat  38665  trlconid  38666  trlcolem  38667  cdlemg42  38670  cdlemg43  38671  cdlemg47a  38675  cdlemg46  38676  cdlemg47  38677  tendoeq1  38705  tendocoval  38707  tendoco2  38709  tendoplco2  38720  tendopltp  38721  cdlemh1  38756  cdlemh2  38757  cdlemi1  38759  cdlemi  38761  cdlemk1  38772  cdlemk2  38773  cdlemk3  38774  cdlemk4  38775  cdlemk8  38779  cdlemk9  38780  cdlemk9bN  38781  cdlemk31  38837  cdlemk28-3  38849  cdlemk19xlem  38883  cdlemk39u  38909  cdlemk19u  38911  cdlemk56w  38914  cdlemn7  39144  cdlemn8  39145  cdlemn9  39146  dihordlem6  39154  dihordlem7  39155  dihordlem7b  39156  dihord1  39159  dihord2a  39160  dihord11c  39165  dihord2pre  39166  dihord2pre2  39167  dihlsscpre  39175  dihord4  39199  dihord6b  39201  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetcN  39243  dihmeetbclemN  39245  dihmeetlem3N  39246  dihmeetlem9N  39256  dihmeetlem13N  39260  dihmeetlem20N  39267  mapdpglem24  39645  mapdpglem32  39646  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  mapdh9aOLDN  39731  hdmap14lem6  39814  nnadddir  40221  sn-addid2  40308  mzpmfp  40485  mzpsubst  40486  pellexlem5  40571  pell14qrexpclnn0  40604  pellfundex  40624  qirropth  40646  monotuz  40679  congmul  40705  congsub  40708  mzpcong  40710  fzmaxdif  40719  jm2.15nn0  40741  idomsubgmo  40939  trclimalb2  41223  mnringmulrcld  41735  fourierdlem42  43580  fourierdlem48  43585  fourierdlem80  43617  prmdvdsfmtnof1lem1  44924  lidldomn1  45367  rngccatidALTV  45435  ringccatidALTV  45498  coe1sclmulval  45614  line2  45986  line2xlem  45987  line2x  45988  line2y  45989  itsclc0yqsol  45998  seposep  46107  iscnrm3rlem8  46129  iscnrm3llem2  46132