Theorem simp2l 1195

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp12l  1282  simp22l  1288  simp32l  1294  fsnunf  6947  f1oiso2  7105  omeulem2  8209  uniinqs  8377  unxpdomlem3  8724  gruina  10240  dedekind  10803  addid2  10823  subaddmulsub  11103  dmdcan  11350  xaddass  12643  xaddass2  12644  xlt2add  12654  xmulasslem3  12680  xadddi2  12691  xadddi2r  12692  expaddzlem  13473  expaddz  13474  expmulz  13476  expdiv  13481  expmordi  13532  modexp  13600  pfxeq  14058  ccatopth2  14079  swrdco  14199  o1add  14970  o1mul  14971  o1sub  14972  fsumsplitsnun  15110  ntrivcvgmul  15258  prmexpb  16062  pcpremul  16180  pcdiv  16189  pcqmul  16190  pcqdiv  16194  4sqlem12  16292  f1ocpbllem  16797  ercpbl  16822  erlecpbl  16823  latjlej12  17677  latmlem12  17693  latj4  17711  latj4rot  17712  gsumsgrpccat  18004  gsmsymgreqlem2  18559  symgsssg  18595  symgfisg  18596  mndodcong  18670  cmn4  18926  ablsub4  18933  abladdsub4  18934  lsm4  18980  abvdom  19609  abvres  19610  abvtrivd  19611  lspsnvs  19886  lspsneu  19895  lspfixed  19900  lspexch  19901  lsmcv  19913  lspsolvlem  19914  coe1sclmulfv  20451  matvscacell  21045  m1detdiag  21206  cramerimplem3  21294  cnprest  21897  hausnei2  21961  isreg2  21985  cmpcld  22010  llyrest  22093  nllyrest  22094  elptr  22181  basqtop  22319  hausflimlem  22587  tmdgsum  22703  utop2nei  22859  trcfilu  22903  ssblps  23032  ssbl  23033  prdsxmslem2  23139  tgqioo  23408  metnrm  23470  bndth  23562  ncvspi  23760  ncvs1  23761  cph2ass  23817  lmmbr2  23862  iscau3  23881  bcthlem5  23931  ovolunlem2  24099  dvres2  24510  dvfsumlem2  24624  plyadd  24807  plymul  24808  coeeu  24815  coemullem  24840  aalioulem4  24924  mulcxp  25268  cxplea  25279  cxple2  25280  cxplt2  25281  cxpcn3lem  25328  angcan  25380  ang180lem5  25391  divsqrtsumlem  25557  logexprlim  25801  dchrvmasumlema  26076  dchrisum0lema  26090  logdivsum  26109  log2sumbnd  26120  abvcxp  26191  padicabv  26206  tghilberti2  26424  brbtwn2  26691  axcontlem4  26753  axcontlem8  26757  clwlkl1loop  27564  clwwlknonex2lem2  27887  clwlknon2num  28147  numclwlk1lem2  28149  chscllem4  29417  orngmul  30876  measxun2  31469  measun  31470  mbfmco2  31523  probun  31677  satfv1fvfmla1  32670  fpr3g  33122  nolesgn2ores  33179  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem2  33209  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd1lem6  33213  scutbdaylt  33276  cgrcomim  33450  cgrcoml  33457  cgrcomr  33458  cgrdegen  33465  btwnintr  33480  btwnexch3  33481  btwnouttr2  33483  btwnouttr  33485  btwnexch  33486  btwndiff  33488  lineid  33544  idinside  33545  btwnconn1lem7  33554  btwnconn1lem8  33555  btwnconn1lem9  33556  btwnconn1lem12  33559  btwnconn1lem14  33561  btwnconn3  33564  midofsegid  33565  segcon2  33566  brsegle2  33570  btwnoutside  33586  outsideoftr  33590  outsideofeu  33592  linethru  33614  cnres2  35056  heibor  35114  lsmsat  36159  lkrlsp  36253  lkrlsp2  36254  lkrlsp3  36255  latm4  36384  omlspjN  36412  hlatj4  36525  4noncolr3  36604  4noncolr2  36605  4noncolr1  36606  athgt  36607  3dimlem3a  36611  3dimlem4a  36614  3dimlem4  36615  3dimlem4OLDN  36616  3dim3  36620  1cvratex  36624  hlatexch4  36632  3atlem4  36637  atcvrlln2  36670  atcvrlln  36671  lplnnlelln  36694  lvoli2  36732  lvolnlelln  36735  lvolnlelpln  36736  4atlem11b  36759  4atlem12b  36762  2lplnja  36770  2lplnj  36771  dalemyeo  36783  dath2  36888  lncvrat  36933  cdlemblem  36944  cdlemb  36945  elpaddri  36953  padd4N  36991  llnmod2i2  37014  llnexchb2  37020  dalawlem1  37022  dalawlem2  37023  pclfinN  37051  osumcllem6N  37112  pexmidlem3N  37123  lhp2lt  37152  lhp2at0  37183  lhp2atnle  37184  lhp2atne  37185  lhp2at0nle  37186  lhp2at0ne  37187  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  lhple  37193  lhpat  37194  lhpat3  37197  ltrncoelN  37294  ltrncoat  37295  ltrncnv  37297  trlat  37320  trl0  37321  ltrnnidn  37325  trlnid  37330  cdlemd7  37355  cdleme0b  37363  cdleme0c  37364  cdleme0fN  37369  cdleme02N  37373  cdleme0ex1N  37374  cdleme0ex2N  37375  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme8  37401  cdleme11a  37411  cdleme17c  37439  cdleme22gb  37445  cdlemeda  37449  cdleme20k  37470  cdleme21a  37476  cdleme21d  37481  cdleme22f2  37498  cdleme22g  37499  cdleme23a  37500  cdleme23b  37501  cdleme23c  37502  cdleme24  37503  cdleme28  37524  cdlemefrs32fva1  37552  cdlemefr32sn2aw  37555  cdlemefs32sn1aw  37565  cdleme41sn3a  37584  cdleme32fva  37588  cdleme32fva1  37589  cdleme35a  37599  cdleme35b  37601  cdleme35c  37602  cdleme35f  37605  cdleme39a  37616  cdleme42a  37622  cdleme42c  37623  cdleme42b  37629  cdleme42e  37630  cdleme42f  37631  cdleme42g  37632  cdleme42h  37633  cdleme43bN  37641  cdleme46f2g2  37644  cdleme17d2  37646  cdleme17d4  37648  cdleme48fv  37650  cdleme48fvg  37651  cdleme4gfv  37658  cdlemeg46c  37664  cdlemeg46nlpq  37668  cdlemeg46gfre  37683  cdleme48d  37686  cdlemeg49lebilem  37690  cdleme50trn2  37702  cdleme50ltrn  37708  cdleme  37711  cdlemf1  37712  cdlemf  37714  trlord  37720  ltrniotacnvval  37733  ltrniotavalbN  37735  cdlemg1cex  37739  cdlemg2dN  37741  cdlemg2ce  37743  cdlemg2fvlem  37745  cdlemg2idN  37747  cdlemg2kq  37753  cdlemg2l  37754  cdlemg2m  37755  cdlemg4b2  37761  cdlemg7fvN  37775  cdlemg8a  37778  cdlemg10bALTN  37787  cdlemg11aq  37789  cdlemg12d  37797  cdlemg13a  37802  cdlemg13  37803  cdlemg14f  37804  cdlemg14g  37805  cdlemg17a  37812  cdlemg17b  37813  cdlemg27a  37843  cdlemg31b0N  37845  cdlemg31a  37848  cdlemg31b  37849  cdlemg31c  37850  ltrnco  37870  trlcoabs  37872  trlcoabs2N  37873  trlcocnvat  37875  trlconid  37876  trlcolem  37877  trlcone  37879  cdlemg42  37880  cdlemg43  37881  cdlemg46  37886  cdlemg47  37887  tendoeq1  37915  tendoco2  37919  tendoplco2  37930  tendopltp  37931  cdlemh1  37966  cdlemh2  37967  cdlemi1  37969  cdlemi  37971  cdlemk1  37982  cdlemk2  37983  cdlemk3  37984  cdlemk4  37985  cdlemk8  37989  cdlemk9  37990  cdlemk9bN  37991  cdlemk31  38047  cdlemk32  38048  cdlemk28-3  38059  cdlemk19u  38121  cdlemk56w  38124  tendoex  38126  erngdvlem4  38142  erngdvlem4-rN  38150  dia11N  38199  dib11N  38311  cdlemn6  38353  cdlemn7  38354  cdlemn8  38355  cdlemn9  38356  dihordlem6  38364  dihordlem7  38365  dihord1  38369  dihord2a  38370  dihord2b  38371  dihord2pre  38376  dihord2pre2  38377  dihlsscpre  38385  dihvalcq2  38398  dihopelvalcpre  38399  dihord4  38409  dihord6b  38411  dihmeetlem1N  38441  dihglblem3N  38446  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetcN  38453  dihmeetbclemN  38455  dihmeetlem4preN  38457  dihjatc1  38462  dihjatc2N  38463  dihjatc3  38464  dihmeetlem9N  38466  dihmeetlem13N  38470  dihmeetlem20N  38477  dih1dimatlem0  38479  mapdpglem24  38855  mapdpglem32  38856  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  mapdh9aOLDN  38941  hdmap14lem6  39024  nnadddir  39212  sn-addid2  39283  mzpsubst  39394  pellexlem5  39479  pellex  39481  pell14qrexpclnn0  39512  pellfundex  39532  qirropth  39554  monotuz  39587  congtr  39611  congmul  39613  congsub  39616  mzpcong  39618  fzmaxdif  39627  jm2.15nn0  39649  idomsubgmo  39847  iunrelexpmin1  40102  iunrelexpmin2  40106  trclimalb2  40120  fourierdlem42  42483  fourierdlem48  42488  fourierdlem80  42520  smfaddlem1  43088  prmdvdsfmtnof1lem1  43795  uspgropssxp  44068  lidldomn1  44241  rngccatidALTV  44309  coe1sclmulval  44488  lincdifsn  44528