Theorem simp2l 1198

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2l	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 482	. 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 206  df-an 396  df-3an 1088

This theorem is referenced by:  simp12l  1285  simp22l  1291  simp32l  1297  fsnunf  7185  f1oiso2  7352  fpr3g  8273  omeulem2  8586  uniinqs  8794  unxpdomlem3  9255  gruina  10816  dedekind  11382  addlid  11402  subaddmulsub  11682  dmdcan  11929  xaddass  13233  xaddass2  13234  xlt2add  13244  xmulasslem3  13270  xadddi2  13281  xadddi2r  13282  expaddzlem  14076  expaddz  14077  expmulz  14079  expdiv  14084  expmordi  14137  modexp  14206  pfxeq  14651  ccatopth2  14672  swrdco  14793  o1add  15563  o1mul  15564  o1sub  15565  fsumsplitsnun  15706  ntrivcvgmul  15853  prmexpb  16662  pcpremul  16781  pcdiv  16790  pcqmul  16791  pcqdiv  16795  4sqlem12  16894  f1ocpbllem  17475  ercpbl  17500  erlecpbl  17501  latjlej12  18413  latmlem12  18429  latj4  18447  latj4rot  18448  gsumsgrpccat  18758  gsmsymgreqlem2  19341  symgsssg  19377  symgfisg  19378  mndodcong  19452  cmn4  19711  ablsub4  19720  abladdsub4  19721  lsm4  19770  abvdom  20590  abvres  20591  abvtrivd  20592  lspsnvs  20873  lspsneu  20882  lspfixed  20887  lspexch  20888  lsmcv  20900  lspsolvlem  20901  ring2idlqus1  21079  coe1sclmulfv  22026  matvscacell  22159  m1detdiag  22320  cramerimplem3  22408  cnprest  23014  hausnei2  23078  isreg2  23102  cmpcld  23127  llyrest  23210  nllyrest  23211  elptr  23298  basqtop  23436  hausflimlem  23704  tmdgsum  23820  utop2nei  23976  trcfilu  24020  ssblps  24149  ssbl  24150  prdsxmslem2  24259  tgqioo  24537  metnrm  24599  bndth  24705  ncvspi  24905  ncvs1  24906  cph2ass  24962  lmmbr2  25008  iscau3  25027  bcthlem5  25077  ovolunlem2  25248  dvres2  25662  dvfsumlem2  25780  plyadd  25967  plymul  25968  coeeu  25975  coemullem  26000  aalioulem4  26085  mulcxp  26430  cxplea  26441  cxple2  26442  cxplt2  26443  cxpcn3lem  26492  angcan  26544  ang180lem5  26555  divsqrtsumlem  26721  logexprlim  26965  dchrvmasumlema  27240  dchrisum0lema  27254  logdivsum  27273  log2sumbnd  27284  abvcxp  27355  padicabv  27370  nolesgn2ores  27412  nosupres  27447  nosupbnd1lem1  27448  nosupbnd1lem2  27449  nosupbnd1lem4  27451  nosupbnd1lem5  27452  nosupbnd1lem6  27453  noinffv  27461  noinfres  27462  noinfbnd1lem1  27463  noinfbnd1lem2  27464  noinfbnd1lem4  27466  noinfbnd1lem6  27468  nosupinfsep  27472  scutbdaylt  27557  tghilberti2  28157  brbtwn2  28431  axcontlem4  28493  axcontlem8  28497  clwlkl1loop  29308  clwwlknonex2lem2  29629  clwlknon2num  29889  numclwlk1lem2  29891  chscllem4  31161  orngmul  32692  measxun2  33507  measun  33508  mbfmco2  33563  probun  33717  satfv1fvfmla1  34713  cgrcomim  35266  cgrcoml  35273  cgrcomr  35274  cgrdegen  35281  btwnintr  35296  btwnexch3  35297  btwnouttr2  35299  btwnouttr  35301  btwnexch  35302  btwndiff  35304  lineid  35360  idinside  35361  btwnconn1lem7  35370  btwnconn1lem8  35371  btwnconn1lem9  35372  btwnconn1lem12  35375  btwnconn1lem14  35377  btwnconn3  35380  midofsegid  35381  segcon2  35382  brsegle2  35386  btwnoutside  35402  outsideoftr  35406  outsideofeu  35408  linethru  35430  gg-dvfsumlem2  35470  cnres2  36935  heibor  36993  lsmsat  38182  lkrlsp  38276  lkrlsp2  38277  lkrlsp3  38278  latm4  38407  omlspjN  38435  hlatj4  38548  4noncolr3  38628  4noncolr2  38629  4noncolr1  38630  athgt  38631  3dimlem3a  38635  3dimlem4a  38638  3dimlem4  38639  3dimlem4OLDN  38640  3dim3  38644  1cvratex  38648  hlatexch4  38656  3atlem4  38661  atcvrlln2  38694  atcvrlln  38695  lplnnlelln  38718  lvoli2  38756  lvolnlelln  38759  lvolnlelpln  38760  4atlem11b  38783  4atlem12b  38786  2lplnja  38794  2lplnj  38795  dalemyeo  38807  dath2  38912  lncvrat  38957  cdlemblem  38968  cdlemb  38969  elpaddri  38977  padd4N  39015  llnmod2i2  39038  llnexchb2  39044  dalawlem1  39046  dalawlem2  39047  pclfinN  39075  osumcllem6N  39136  pexmidlem3N  39147  lhp2lt  39176  lhp2at0  39207  lhp2atnle  39208  lhp2atne  39209  lhp2at0nle  39210  lhp2at0ne  39211  lhpelim  39212  lhpmod2i2  39213  lhpmod6i1  39214  lhple  39217  lhpat  39218  lhpat3  39221  ltrncoelN  39318  ltrncoat  39319  ltrncnv  39321  trlat  39344  trl0  39345  ltrnnidn  39349  trlnid  39354  cdlemd7  39379  cdleme0b  39387  cdleme0c  39388  cdleme0fN  39393  cdleme02N  39397  cdleme0ex1N  39398  cdleme0ex2N  39399  cdleme7aa  39417  cdleme7c  39420  cdleme7d  39421  cdleme7e  39422  cdleme7ga  39423  cdleme7  39424  cdleme8  39425  cdleme11a  39435  cdleme17c  39463  cdleme22gb  39469  cdlemeda  39473  cdleme20k  39494  cdleme21a  39500  cdleme21d  39505  cdleme22f2  39522  cdleme22g  39523  cdleme23a  39524  cdleme23b  39525  cdleme23c  39526  cdleme24  39527  cdleme28  39548  cdlemefrs32fva1  39576  cdlemefr32sn2aw  39579  cdlemefs32sn1aw  39589  cdleme41sn3a  39608  cdleme32fva  39612  cdleme32fva1  39613  cdleme35a  39623  cdleme35b  39625  cdleme35c  39626  cdleme35f  39629  cdleme39a  39640  cdleme42a  39646  cdleme42c  39647  cdleme42b  39653  cdleme42e  39654  cdleme42f  39655  cdleme42g  39656  cdleme42h  39657  cdleme43bN  39665  cdleme46f2g2  39668  cdleme17d2  39670  cdleme17d4  39672  cdleme48fv  39674  cdleme48fvg  39675  cdleme4gfv  39682  cdlemeg46c  39688  cdlemeg46nlpq  39692  cdlemeg46gfre  39707  cdleme48d  39710  cdlemeg49lebilem  39714  cdleme50trn2  39726  cdleme50ltrn  39732  cdleme  39735  cdlemf1  39736  cdlemf  39738  trlord  39744  ltrniotacnvval  39757  ltrniotavalbN  39759  cdlemg1cex  39763  cdlemg2dN  39765  cdlemg2ce  39767  cdlemg2fvlem  39769  cdlemg2idN  39771  cdlemg2kq  39777  cdlemg2l  39778  cdlemg2m  39779  cdlemg4b2  39785  cdlemg7fvN  39799  cdlemg8a  39802  cdlemg10bALTN  39811  cdlemg11aq  39813  cdlemg12d  39821  cdlemg13a  39826  cdlemg13  39827  cdlemg14f  39828  cdlemg14g  39829  cdlemg17a  39836  cdlemg17b  39837  cdlemg27a  39867  cdlemg31b0N  39869  cdlemg31a  39872  cdlemg31b  39873  cdlemg31c  39874  ltrnco  39894  trlcoabs  39896  trlcoabs2N  39897  trlcocnvat  39899  trlconid  39900  trlcolem  39901  trlcone  39903  cdlemg42  39904  cdlemg43  39905  cdlemg46  39910  cdlemg47  39911  tendoeq1  39939  tendoco2  39943  tendoplco2  39954  tendopltp  39955  cdlemh1  39990  cdlemh2  39991  cdlemi1  39993  cdlemi  39995  cdlemk1  40006  cdlemk2  40007  cdlemk3  40008  cdlemk4  40009  cdlemk8  40013  cdlemk9  40014  cdlemk9bN  40015  cdlemk31  40071  cdlemk32  40072  cdlemk28-3  40083  cdlemk19u  40145  cdlemk56w  40148  tendoex  40150  erngdvlem4  40166  erngdvlem4-rN  40174  dia11N  40223  dib11N  40335  cdlemn6  40377  cdlemn7  40378  cdlemn8  40379  cdlemn9  40380  dihordlem6  40388  dihordlem7  40389  dihord1  40393  dihord2a  40394  dihord2b  40395  dihord2pre  40400  dihord2pre2  40401  dihlsscpre  40409  dihvalcq2  40422  dihopelvalcpre  40423  dihord4  40433  dihord6b  40435  dihmeetlem1N  40465  dihglblem3N  40470  dihmeetlem2N  40474  dihglbcpreN  40475  dihmeetcN  40477  dihmeetbclemN  40479  dihmeetlem4preN  40481  dihjatc1  40486  dihjatc2N  40487  dihjatc3  40488  dihmeetlem9N  40490  dihmeetlem13N  40494  dihmeetlem20N  40501  dih1dimatlem0  40503  mapdpglem24  40879  mapdpglem32  40880  baerlem3lem2  40885  baerlem5alem2  40886  baerlem5blem2  40887  mapdh9aOLDN  40965  hdmap14lem6  41048  nnadddir  41487  sn-addlid  41580  mzpsubst  41789  pellexlem5  41874  pellex  41876  pell14qrexpclnn0  41907  pellfundex  41927  qirropth  41949  monotuz  41983  congtr  42007  congmul  42009  congsub  42012  mzpcong  42014  fzmaxdif  42023  jm2.15nn0  42045  idomsubgmo  42243  iunrelexpmin1  42762  iunrelexpmin2  42766  trclimalb2  42780  mnringmulrcld  43290  fourierdlem42  45164  fourierdlem48  45169  fourierdlem80  45201  smfaddlem1  45778  prmdvdsfmtnof1lem1  46551  uspgropssxp  46821  lidldomn1  46912  rngccatidALTV  46976  coe1sclmulval  47154  lincdifsn  47193  seposep  47646  iscnrm3rlem8  47668  iscnrm3llem2  47671