Theorem simp2l 1192

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  simp12l  1279  simp22l  1285  simp32l  1291  fsnunf  6814  f1oiso2  6968  omeulem2  8059  uniinqs  8227  unxpdomlem3  8570  gruina  10086  dedekind  10650  addid2  10670  subaddmulsub  10951  dmdcan  11198  xaddass  12492  xaddass2  12493  xlt2add  12503  xmulasslem3  12529  xadddi2  12540  xadddi2r  12541  expaddzlem  13322  expaddz  13323  expmulz  13325  expdiv  13330  expmordi  13381  modexp  13449  ccatopth2  13915  swrdco  14035  o1add  14804  o1mul  14805  o1sub  14806  fsumsplitsnun  14943  ntrivcvgmul  15091  prmexpb  15891  pcpremul  16009  pcdiv  16018  pcqmul  16019  pcqdiv  16023  4sqlem12  16121  f1ocpbllem  16626  ercpbl  16651  erlecpbl  16652  latjlej12  17506  latmlem12  17522  latj4  17540  latj4rot  17541  symgsssg  18326  symgfisg  18327  mndodcong  18401  cmn4  18652  ablsub4  18658  abladdsub4  18659  lsm4  18703  abvdom  19299  abvres  19300  abvtrivd  19301  lspsnvs  19576  lspsneu  19585  lspfixed  19590  lspexch  19591  lsmcv  19603  lspsolvlem  19604  coe1sclmulfv  20134  matvscacell  20729  m1detdiag  20890  cramerimplem3  20978  cnprest  21581  hausnei2  21645  isreg2  21669  cmpcld  21694  llyrest  21777  nllyrest  21778  elptr  21865  basqtop  22003  hausflimlem  22271  tmdgsum  22387  utop2nei  22542  trcfilu  22586  ssblps  22715  ssbl  22716  prdsxmslem2  22822  tgqioo  23091  metnrm  23153  bndth  23245  ncvspi  23443  ncvs1  23444  cph2ass  23500  lmmbr2  23545  iscau3  23564  bcthlem5  23614  ovolunlem2  23782  dvres2  24193  dvfsumlem2  24307  plyadd  24490  plymul  24491  coeeu  24498  coemullem  24523  aalioulem4  24607  mulcxp  24949  cxplea  24960  cxple2  24961  cxplt2  24962  cxpcn3lem  25009  angcan  25061  ang180lem5  25072  divsqrtsumlem  25239  logexprlim  25483  dchrvmasumlema  25758  dchrisum0lema  25772  logdivsum  25791  log2sumbnd  25802  abvcxp  25873  padicabv  25888  tghilberti2  26106  brbtwn2  26374  axcontlem4  26436  axcontlem8  26440  clwlkl1loop  27251  clwwlkel  27512  clwwlknonex2lem2  27574  clwlknon2num  27839  numclwlk1lem2  27841  chscllem4  29108  orngmul  30530  measxun2  31086  measun  31087  mbfmco2  31140  probun  31294  satfv1fvfmla1  32279  fpr3g  32732  nolesgn2ores  32789  nosupres  32817  nosupbnd1lem1  32818  nosupbnd1lem2  32819  nosupbnd1lem4  32821  nosupbnd1lem5  32822  nosupbnd1lem6  32823  scutbdaylt  32886  cgrcomim  33060  cgrcoml  33067  cgrcomr  33068  cgrdegen  33075  btwnintr  33090  btwnexch3  33091  btwnouttr2  33093  btwnouttr  33095  btwnexch  33096  btwndiff  33098  lineid  33154  idinside  33155  btwnconn1lem7  33164  btwnconn1lem8  33165  btwnconn1lem9  33166  btwnconn1lem12  33169  btwnconn1lem14  33171  btwnconn3  33174  midofsegid  33175  segcon2  33176  brsegle2  33180  btwnoutside  33196  outsideoftr  33200  outsideofeu  33202  linethru  33224  cnres2  34592  heibor  34650  lsmsat  35694  lkrlsp  35788  lkrlsp2  35789  lkrlsp3  35790  latm4  35919  omlspjN  35947  hlatj4  36060  4noncolr3  36139  4noncolr2  36140  4noncolr1  36141  athgt  36142  3dimlem3a  36146  3dimlem4a  36149  3dimlem4  36150  3dimlem4OLDN  36151  3dim3  36155  1cvratex  36159  hlatexch4  36167  3atlem4  36172  atcvrlln2  36205  atcvrlln  36206  lplnnlelln  36229  lvoli2  36267  lvolnlelln  36270  lvolnlelpln  36271  4atlem11b  36294  4atlem12b  36297  2lplnja  36305  2lplnj  36306  dalemyeo  36318  dath2  36423  lncvrat  36468  cdlemblem  36479  cdlemb  36480  elpaddri  36488  padd4N  36526  llnmod2i2  36549  llnexchb2  36555  dalawlem1  36557  dalawlem2  36558  pclfinN  36586  osumcllem6N  36647  pexmidlem3N  36658  lhp2lt  36687  lhp2at0  36718  lhp2atnle  36719  lhp2atne  36720  lhp2at0nle  36721  lhp2at0ne  36722  lhpelim  36723  lhpmod2i2  36724  lhpmod6i1  36725  lhple  36728  lhpat  36729  lhpat3  36732  ltrncoelN  36829  ltrncoat  36830  ltrncnv  36832  trlat  36855  trl0  36856  ltrnnidn  36860  trlnid  36865  cdlemd7  36890  cdleme0b  36898  cdleme0c  36899  cdleme0fN  36904  cdleme02N  36908  cdleme0ex1N  36909  cdleme0ex2N  36910  cdleme7aa  36928  cdleme7c  36931  cdleme7d  36932  cdleme7e  36933  cdleme7ga  36934  cdleme7  36935  cdleme8  36936  cdleme11a  36946  cdleme17c  36974  cdleme22gb  36980  cdlemeda  36984  cdleme20k  37005  cdleme21a  37011  cdleme21d  37016  cdleme22f2  37033  cdleme22g  37034  cdleme23a  37035  cdleme23b  37036  cdleme23c  37037  cdleme24  37038  cdleme28  37059  cdlemefrs32fva1  37087  cdlemefr32sn2aw  37090  cdlemefs32sn1aw  37100  cdleme41sn3a  37119  cdleme32fva  37123  cdleme32fva1  37124  cdleme35a  37134  cdleme35b  37136  cdleme35c  37137  cdleme35f  37140  cdleme39a  37151  cdleme42a  37157  cdleme42c  37158  cdleme42b  37164  cdleme42e  37165  cdleme42f  37166  cdleme42g  37167  cdleme42h  37168  cdleme43bN  37176  cdleme46f2g2  37179  cdleme17d2  37181  cdleme17d4  37183  cdleme48fv  37185  cdleme48fvg  37186  cdleme4gfv  37193  cdlemeg46c  37199  cdlemeg46nlpq  37203  cdlemeg46gfre  37218  cdleme48d  37221  cdlemeg49lebilem  37225  cdleme50trn2  37237  cdleme50ltrn  37243  cdleme  37246  cdlemf1  37247  cdlemf  37249  trlord  37255  ltrniotacnvval  37268  ltrniotavalbN  37270  cdlemg1cex  37274  cdlemg2dN  37276  cdlemg2ce  37278  cdlemg2fvlem  37280  cdlemg2idN  37282  cdlemg2kq  37288  cdlemg2l  37289  cdlemg2m  37290  cdlemg4b2  37296  cdlemg7fvN  37310  cdlemg8a  37313  cdlemg10bALTN  37322  cdlemg11aq  37324  cdlemg12d  37332  cdlemg13a  37337  cdlemg13  37338  cdlemg14f  37339  cdlemg14g  37340  cdlemg17a  37347  cdlemg17b  37348  cdlemg27a  37378  cdlemg31b0N  37380  cdlemg31a  37383  cdlemg31b  37384  cdlemg31c  37385  ltrnco  37405  trlcoabs  37407  trlcoabs2N  37408  trlcocnvat  37410  trlconid  37411  trlcolem  37412  trlcone  37414  cdlemg42  37415  cdlemg43  37416  cdlemg46  37421  cdlemg47  37422  tendoeq1  37450  tendoco2  37454  tendoplco2  37465  tendopltp  37466  cdlemh1  37501  cdlemh2  37502  cdlemi1  37504  cdlemi  37506  cdlemk1  37517  cdlemk2  37518  cdlemk3  37519  cdlemk4  37520  cdlemk8  37524  cdlemk9  37525  cdlemk9bN  37526  cdlemk31  37582  cdlemk32  37583  cdlemk28-3  37594  cdlemk19u  37656  cdlemk56w  37659  tendoex  37661  erngdvlem4  37677  erngdvlem4-rN  37685  dia11N  37734  dib11N  37846  cdlemn6  37888  cdlemn7  37889  cdlemn8  37890  cdlemn9  37891  dihordlem6  37899  dihordlem7  37900  dihord1  37904  dihord2a  37905  dihord2b  37906  dihord2pre  37911  dihord2pre2  37912  dihlsscpre  37920  dihvalcq2  37933  dihopelvalcpre  37934  dihord4  37944  dihord6b  37946  dihmeetlem1N  37976  dihglblem3N  37981  dihmeetlem2N  37985  dihglbcpreN  37986  dihmeetcN  37988  dihmeetbclemN  37990  dihmeetlem4preN  37992  dihjatc1  37997  dihjatc2N  37998  dihjatc3  37999  dihmeetlem9N  38001  dihmeetlem13N  38005  dihmeetlem20N  38012  dih1dimatlem0  38014  mapdpglem24  38390  mapdpglem32  38391  baerlem3lem2  38396  baerlem5alem2  38397  baerlem5blem2  38398  mapdh9aOLDN  38476  hdmap14lem6  38559  mzpsubst  38849  pellexlem5  38934  pellex  38936  pell14qrexpclnn0  38967  pellfundex  38987  qirropth  39009  monotuz  39042  congtr  39066  congmul  39068  congsub  39071  mzpcong  39073  fzmaxdif  39082  jm2.15nn0  39104  idomsubgmo  39302  iunrelexpmin1  39557  iunrelexpmin2  39561  trclimalb2  39575  fourierdlem42  41996  fourierdlem48  42001  fourierdlem80  42033  smfaddlem1  42601  prmdvdsfmtnof1lem1  43248  uspgropssxp  43521  lidldomn1  43690  rngccatidALTV  43758  coe1sclmulval  43939  lincdifsn  43979