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  7216  f1resrcmplf1d  7305  f1oiso2  7386  fnsuppres  8239  frrlem4  8338  omeulem2  8622  uniinqs  8849  unxpdomlem3  9280  sup0  9489  fin23lem11  10425  reclem3pr  11164  dedekind  11503  addlid  11523  subaddmulsub  11809  dmdcan  12057  nnadddir  12424  xaddass2  13410  xlt2add  13420  xadddi2  13457  expaddzlem  14278  expaddz  14279  expmulz  14281  expdiv  14286  expmordi  14340  pfxeq  14876  ccatopth2  14897  relexpaddnn  15236  o1add  15813  o1mul  15814  o1sub  15815  ntrivcvgmul  16103  prmexpb  16927  pcpremul  17053  pcdiv  17062  pcqmul  17063  pcqdiv  17067  4sqlem12  17166  f1ocpbllem  17728  ercpbl  17753  erlecpbl  17754  latjlej12  18661  latmlem12  18677  latj4  18695  gsumsgrpccat  19068  symgsssg  19714  symgfisg  19715  mndodcong  19789  cmn4  20048  ablsub4  20057  abladdsub4  20058  lsm4  20107  abvdom  21120  abvtrivd  21122  orngmul  21155  lspsnvs  21425  lspsneu  21434  lspfixed  21439  lspexch  21440  lsmcv  21452  lspsolvlem  21453  mvrf1  22326  coe1sclmulfv  22635  m1detdiag  22945  cnprest  23640  isreg2  23728  elptr  23925  hausflimlem  24331  trcfilu  24645  ssblps  24774  ssbl  24775  prdsxmslem2  24881  tgqioo  25152  metnrm  25215  bndth  25312  ncvspi  25510  cph2ass  25567  iscau3  25632  ovolunlem2  25852  dvres2  26265  dvfsumlem2  26380  dvfsum2  26387  deg1tm  26470  plyadd  26569  plymul  26570  coeeu  26577  coemullem  26602  aalioulem4  26695  cxplea  27057  cxple2  27058  cxplt2  27059  cxple2a  27060  cxpcn3lem  27108  angcan  27163  ang180lem5  27174  divsqrtsumlem  27340  logexprlim  27585  dchrvmasumlema  27860  dchrisum0lema  27874  logdivsum  27893  log2sumbnd  27904  padicabv  27990  nolesgn2ores  28062  nogesgn1o  28063  nogesgn1ores  28064  nolt02o  28085  nogt01o  28086  nosupinfsep  28122  noetalem1  28131  noeta2  28180  cutbdaylt  28217  expsgt0  28856  bdayfinbndlem1  28886  tghilberti2  29139  brbtwn2  29516  axcontlem4  29578  axcontlem8  29582  clwlkl1loop  30403  umgr2cycllem  30779  chscllem4  32275  mdslmd4i  32968  nexple  33497  measxun2  34926  measun  34927  mbfmco2  34980  probun  35134  satfv1fvfmla1  36368  wsuclem  36778  cgrcomim  36945  cgrcoml  36952  cgrcomr  36953  cgrdegen  36960  btwnintr  36975  btwnexch3  36976  btwnouttr  36980  btwnexch  36981  btwndiff  36983  ifscgr  37000  lineid  37039  btwnconn1lem7  37049  btwnconn1lem8  37050  btwnconn1lem9  37051  btwnconn1lem12  37054  midofsegid  37060  brsegle2  37065  btwnoutside  37081  outsideoftr  37085  ttcmin  37475  cnres2  38900  heibor  38958  lsmsat  40268  lkrlsp  40362  lkrlsp2  40363  lkrlsp3  40364  lshpkrlem6  40375  latm4  40493  omlspjN  40521  hlatj4  40634  4noncolr3  40713  4noncolr2  40714  4noncolr1  40715  3dimlem3a  40720  3dimlem4a  40723  3dimlem4  40724  3dimlem4OLDN  40725  1cvratex  40733  hlatexch4  40741  3atlem4  40746  atcvrlln2  40779  atcvrlln  40780  llnmlplnN  40799  lplnnlelln  40803  lvoli2  40841  lvolnlelln  40844  lvolnlelpln  40845  4atlem11b  40868  4atlem12b  40871  2lplnj  40880  dalemzeo  40893  dath2  40997  lncvrat  41042  cdlemb  41054  elpaddri  41062  padd4N  41100  llnmod2i2  41123  llnexchb2  41129  dalawlem1  41131  dalawlem2  41132  osumcllem6N  41221  pexmidlem3N  41232  pexmidlem4N  41233  lhp2lt  41261  lhp2at0  41292  lhp2atne  41294  lhp2at0ne  41296  lhpmod2i2  41298  lhpmod6i1  41299  lhpat  41303  lhpat3  41306  4atexlemex6  41334  ltrncoval  41405  ltrncnv  41406  ltrnnidn  41434  cdlemd7  41464  cdleme0b  41472  cdleme0c  41473  cdleme0fN  41478  cdleme0ex1N  41483  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme11a  41520  cdleme17c  41548  cdleme22gb  41554  cdlemeda  41558  cdleme20k  41579  cdleme21a  41585  cdleme21at  41588  cdleme21d  41590  cdleme22f2  41607  cdleme22g  41608  cdleme24  41612  cdleme28  41633  cdlemefrs29cpre1  41658  cdlemefr29exN  41662  cdlemefr32sn2aw  41664  cdleme32fva  41697  cdleme32fva1  41698  cdleme35a  41708  cdleme42c  41732  cdleme42e  41739  cdleme42f  41740  cdleme42g  41741  cdleme42h  41742  cdleme43bN  41750  cdleme46f2g2  41753  cdleme17d2  41755  cdleme4gfv  41767  cdlemeg46c  41773  cdlemeg46nlpq  41777  cdlemeg46gfre  41792  cdlemeg49lebilem  41799  cdleme50trn1  41809  cdleme50trn2  41811  cdleme50ltrn  41817  cdleme  41820  cdlemf1  41821  cdlemf  41823  trlord  41829  ltrniotavalbN  41844  cdlemg1cex  41848  cdlemg2dN  41850  cdlemg2ce  41852  cdlemg2fvlem  41854  cdlemg2idN  41856  cdlemg2kq  41862  cdlemg2l  41863  cdlemg7fvN  41884  cdlemg7aN  41885  cdlemg8a  41887  cdlemg11aq  41898  cdlemg12d  41906  cdlemg13a  41911  cdlemg13  41912  cdlemg14f  41913  cdlemg14g  41914  cdlemg17b  41922  cdlemg27a  41952  cdlemg31b0N  41954  cdlemg31a  41957  cdlemg31b  41958  cdlemg31c  41959  ltrnco  41979  trlcoabs2N  41982  trlcocnvat  41984  trlconid  41985  trlcolem  41986  cdlemg42  41989  cdlemg43  41990  cdlemg47a  41994  cdlemg46  41995  cdlemg47  41996  tendoeq1  42024  tendocoval  42026  tendoco2  42028  tendoplco2  42039  tendopltp  42040  cdlemh1  42075  cdlemh2  42076  cdlemi1  42078  cdlemi  42080  cdlemk1  42091  cdlemk2  42092  cdlemk3  42093  cdlemk4  42094  cdlemk8  42098  cdlemk9  42099  cdlemk9bN  42100  cdlemk31  42156  cdlemk28-3  42168  cdlemk19xlem  42202  cdlemk39u  42228  cdlemk19u  42230  cdlemk56w  42233  cdlemn7  42463  cdlemn8  42464  cdlemn9  42465  dihordlem6  42473  dihordlem7  42474  dihordlem7b  42475  dihord1  42478  dihord2a  42479  dihord11c  42484  dihord2pre  42485  dihord2pre2  42486  dihlsscpre  42494  dihord4  42518  dihord6b  42520  dihmeetlem2N  42559  dihglbcpreN  42560  dihmeetcN  42562  dihmeetbclemN  42564  dihmeetlem3N  42565  dihmeetlem9N  42575  dihmeetlem13N  42579  dihmeetlem20N  42586  mapdpglem24  42964  mapdpglem32  42965  baerlem3lem2  42970  baerlem5alem2  42971  baerlem5blem2  42972  mapdh9aOLDN  43050  hdmap14lem6  43133  sn-addlid  43659  mzpmfp  43962  mzpsubst  43963  pellexlem5  44044  pell14qrexpclnn0  44077  pellfundex  44097  qirropth  44119  monotuz  44152  congmul  44178  congsub  44181  mzpcong  44183  fzmaxdif  44192  jm2.15nn0  44214  idomsubgmo  44398  trclimalb2  44929  mnringmulrcld  45429  fourierdlem42  47374  fourierdlem48  47379  fourierdlem80  47411  prmdvdsfmtnof1lem1  48884  cycldlenngric  49241  gpgedgvtx1  49375  lidldomn1  49543  rngccatidALTV  49584  ringccatidALTV  49618  coe1sclmulval  49712  line2  50079  line2xlem  50080  line2x  50081  itsclc0yqsol  50091  seposep  50255  iscnrm3rlem8  50276  iscnrm3llem2  50279