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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp12r  1306  simp22r  1312  simp32r  1318  fsnunf  7185  f1oiso2  7352  fnsuppres  8188  frrlem4  8287  omeulem2  8569  uniinqs  8796  unxpdomlem3  9219  sup0  9428  fin23lem11  10302  reclem3pr  11035  dedekind  11374  addlid  11394  subaddmulsub  11678  dmdcan  11926  nnadddir  12293  xaddass2  13277  xlt2add  13287  xadddi2  13324  expaddzlem  14143  expaddz  14144  expmulz  14146  expdiv  14151  expmordi  14205  pfxeq  14735  ccatopth2  14756  relexpaddnn  15090  o1add  15667  o1mul  15668  o1sub  15669  ntrivcvgmul  15958  prmexpb  16779  pcpremul  16904  pcdiv  16913  pcqmul  16914  pcqdiv  16918  4sqlem12  17017  f1ocpbllem  17579  ercpbl  17604  erlecpbl  17605  latjlej12  18512  latmlem12  18528  latj4  18546  gsumsgrpccat  18900  symgsssg  19538  symgfisg  19539  mndodcong  19613  cmn4  19872  ablsub4  19881  abladdsub4  19882  lsm4  19931  abvdom  20914  abvtrivd  20916  orngmul  20949  lspsnvs  21219  lspsneu  21228  lspfixed  21233  lspexch  21234  lsmcv  21246  lspsolvlem  21247  mvrf1  22116  coe1sclmulfv  22425  m1detdiag  22735  cnprest  23427  isreg2  23515  elptr  23711  hausflimlem  24117  trcfilu  24431  ssblps  24560  ssbl  24561  prdsxmslem2  24667  tgqioo  24938  metnrm  25001  bndth  25098  ncvspi  25296  cph2ass  25353  iscau3  25418  ovolunlem2  25638  dvres2  26052  dvfsumlem2  26167  dvfsum2  26174  deg1tm  26257  plyadd  26355  plymul  26356  coeeu  26363  coemullem  26388  aalioulem4  26479  cxplea  26842  cxple2  26843  cxplt2  26844  cxple2a  26845  cxpcn3lem  26893  angcan  26948  ang180lem5  26959  divsqrtsumlem  27125  logexprlim  27370  dchrvmasumlema  27645  dchrisum0lema  27659  logdivsum  27678  log2sumbnd  27689  padicabv  27775  nolesgn2ores  27817  nogesgn1o  27818  nogesgn1ores  27819  nolt02o  27840  nogt01o  27841  nosupinfsep  27877  noetalem1  27886  noeta2  27935  cutbdaylt  27972  expsgt0  28611  bdayfinbndlem1  28641  tghilberti2  28892  brbtwn2  29236  axcontlem4  29298  axcontlem8  29302  clwlkl1loop  30113  chscllem4  31973  mdslmd4i  32666  nexple  33158  measxun2  34581  measun  34582  mbfmco2  34636  probun  34790  satfv1fvfmla1  35896  wsuclem  36296  cgrcomim  36462  cgrcoml  36469  cgrcomr  36470  cgrdegen  36477  btwnintr  36492  btwnexch3  36493  btwnouttr  36497  btwnexch  36498  btwndiff  36500  ifscgr  36517  lineid  36556  btwnconn1lem7  36566  btwnconn1lem8  36567  btwnconn1lem9  36568  btwnconn1lem12  36571  midofsegid  36577  brsegle2  36582  btwnoutside  36598  outsideoftr  36602  ttcmin  36988  cnres2  38395  heibor  38453  lsmsat  39763  lkrlsp  39857  lkrlsp2  39858  lkrlsp3  39859  lshpkrlem6  39870  latm4  39988  omlspjN  40016  hlatj4  40129  4noncolr3  40208  4noncolr2  40209  4noncolr1  40210  3dimlem3a  40215  3dimlem4a  40218  3dimlem4  40219  3dimlem4OLDN  40220  1cvratex  40228  hlatexch4  40236  3atlem4  40241  atcvrlln2  40274  atcvrlln  40275  llnmlplnN  40294  lplnnlelln  40298  lvoli2  40336  lvolnlelln  40339  lvolnlelpln  40340  4atlem11b  40363  4atlem12b  40366  2lplnj  40375  dalemzeo  40388  dath2  40492  lncvrat  40537  cdlemb  40549  elpaddri  40557  padd4N  40595  llnmod2i2  40618  llnexchb2  40624  dalawlem1  40626  dalawlem2  40627  osumcllem6N  40716  pexmidlem3N  40727  pexmidlem4N  40728  lhp2lt  40756  lhp2at0  40787  lhp2atne  40789  lhp2at0ne  40791  lhpmod2i2  40793  lhpmod6i1  40794  lhpat  40798  lhpat3  40801  4atexlemex6  40829  ltrncoval  40900  ltrncnv  40901  ltrnnidn  40929  cdlemd7  40959  cdleme0b  40967  cdleme0c  40968  cdleme0fN  40973  cdleme0ex1N  40978  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme11a  41015  cdleme17c  41043  cdleme22gb  41049  cdlemeda  41053  cdleme20k  41074  cdleme21a  41080  cdleme21at  41083  cdleme21d  41085  cdleme22f2  41102  cdleme22g  41103  cdleme24  41107  cdleme28  41128  cdlemefrs29cpre1  41153  cdlemefr29exN  41157  cdlemefr32sn2aw  41159  cdleme32fva  41192  cdleme32fva1  41193  cdleme35a  41203  cdleme42c  41227  cdleme42e  41234  cdleme42f  41235  cdleme42g  41236  cdleme42h  41237  cdleme43bN  41245  cdleme46f2g2  41248  cdleme17d2  41250  cdleme4gfv  41262  cdlemeg46c  41268  cdlemeg46nlpq  41272  cdlemeg46gfre  41287  cdlemeg49lebilem  41294  cdleme50trn1  41304  cdleme50trn2  41306  cdleme50ltrn  41312  cdleme  41315  cdlemf1  41316  cdlemf  41318  trlord  41324  ltrniotavalbN  41339  cdlemg1cex  41343  cdlemg2dN  41345  cdlemg2ce  41347  cdlemg2fvlem  41349  cdlemg2idN  41351  cdlemg2kq  41357  cdlemg2l  41358  cdlemg7fvN  41379  cdlemg7aN  41380  cdlemg8a  41382  cdlemg11aq  41393  cdlemg12d  41401  cdlemg13a  41406  cdlemg13  41407  cdlemg14f  41408  cdlemg14g  41409  cdlemg17b  41417  cdlemg27a  41447  cdlemg31b0N  41449  cdlemg31a  41452  cdlemg31b  41453  cdlemg31c  41454  ltrnco  41474  trlcoabs2N  41477  trlcocnvat  41479  trlconid  41480  trlcolem  41481  cdlemg42  41484  cdlemg43  41485  cdlemg47a  41489  cdlemg46  41490  cdlemg47  41491  tendoeq1  41519  tendocoval  41521  tendoco2  41523  tendoplco2  41534  tendopltp  41535  cdlemh1  41570  cdlemh2  41571  cdlemi1  41573  cdlemi  41575  cdlemk1  41586  cdlemk2  41587  cdlemk3  41588  cdlemk4  41589  cdlemk8  41593  cdlemk9  41594  cdlemk9bN  41595  cdlemk31  41651  cdlemk28-3  41663  cdlemk19xlem  41697  cdlemk39u  41723  cdlemk19u  41725  cdlemk56w  41728  cdlemn7  41958  cdlemn8  41959  cdlemn9  41960  dihordlem6  41968  dihordlem7  41969  dihordlem7b  41970  dihord1  41973  dihord2a  41974  dihord11c  41979  dihord2pre  41980  dihord2pre2  41981  dihlsscpre  41989  dihord4  42013  dihord6b  42015  dihmeetlem2N  42054  dihglbcpreN  42055  dihmeetcN  42057  dihmeetbclemN  42059  dihmeetlem3N  42060  dihmeetlem9N  42070  dihmeetlem13N  42074  dihmeetlem20N  42081  mapdpglem24  42459  mapdpglem32  42460  baerlem3lem2  42465  baerlem5alem2  42466  baerlem5blem2  42467  mapdh9aOLDN  42545  hdmap14lem6  42628  sn-addlid  43146  mzpmfp  43461  mzpsubst  43462  pellexlem5  43543  pell14qrexpclnn0  43576  pellfundex  43596  qirropth  43618  monotuz  43651  congmul  43677  congsub  43680  mzpcong  43682  fzmaxdif  43691  jm2.15nn0  43713  idomsubgmo  43903  trclimalb2  44435  mnringmulrcld  44935  fourierdlem42  46846  fourierdlem48  46851  fourierdlem80  46883  prmdvdsfmtnof1lem1  48319  cycldlenngric  48676  gpgedgvtx1  48810  lidldomn1  48979  rngccatidALTV  49020  ringccatidALTV  49054  coe1sclmulval  49148  line2  49515  line2xlem  49516  line2x  49517  line2y  49518  itsclc0yqsol  49527  seposep  49687  iscnrm3rlem8  49708  iscnrm3llem2  49711