Theorem simp2l 1199

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 1134	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp12l  1286  simp22l  1292  simp32l  1298  fsnunf  7219  f1oiso2  7388  fpr3g  8326  omeulem2  8639  uniinqs  8855  unxpdomlem3  9315  gruina  10887  dedekind  11453  addlid  11473  subaddmulsub  11753  dmdcan  12004  xaddass  13311  xaddass2  13312  xlt2add  13322  xmulasslem3  13348  xadddi2  13359  xadddi2r  13360  expaddzlem  14156  expaddz  14157  expmulz  14159  expdiv  14164  expmordi  14217  modexp  14287  pfxeq  14744  ccatopth2  14765  swrdco  14886  o1add  15660  o1mul  15661  o1sub  15662  fsumsplitsnun  15803  ntrivcvgmul  15950  prmexpb  16766  pcpremul  16890  pcdiv  16899  pcqmul  16900  pcqdiv  16904  4sqlem12  17003  f1ocpbllem  17584  ercpbl  17609  erlecpbl  17610  latjlej12  18525  latmlem12  18541  latj4  18559  latj4rot  18560  gsumsgrpccat  18875  gsmsymgreqlem2  19473  symgsssg  19509  symgfisg  19510  mndodcong  19584  cmn4  19843  ablsub4  19852  abladdsub4  19853  lsm4  19902  abvdom  20853  abvres  20854  abvtrivd  20855  lspsnvs  21139  lspsneu  21148  lspfixed  21153  lspexch  21154  lsmcv  21166  lspsolvlem  21167  ring2idlqus1  21352  coe1sclmulfv  22307  matvscacell  22463  m1detdiag  22624  cramerimplem3  22712  cnprest  23318  hausnei2  23382  isreg2  23406  cmpcld  23431  llyrest  23514  nllyrest  23515  elptr  23602  basqtop  23740  hausflimlem  24008  tmdgsum  24124  utop2nei  24280  trcfilu  24324  ssblps  24453  ssbl  24454  prdsxmslem2  24563  tgqioo  24841  metnrm  24903  bndth  25009  ncvspi  25209  ncvs1  25210  cph2ass  25266  lmmbr2  25312  iscau3  25331  bcthlem5  25381  ovolunlem2  25552  dvres2  25967  dvfsumlem2  26087  dvfsumlem2OLD  26088  plyadd  26276  plymul  26277  coeeu  26284  coemullem  26309  aalioulem4  26395  mulcxp  26745  cxplea  26756  cxple2  26757  cxplt2  26758  cxpcn3lem  26808  angcan  26863  ang180lem5  26874  divsqrtsumlem  27041  logexprlim  27287  dchrvmasumlema  27562  dchrisum0lema  27576  logdivsum  27595  log2sumbnd  27606  abvcxp  27677  padicabv  27692  nolesgn2ores  27735  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem2  27772  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd1lem6  27776  noinffv  27784  noinfres  27785  noinfbnd1lem1  27786  noinfbnd1lem2  27787  noinfbnd1lem4  27789  noinfbnd1lem6  27791  nosupinfsep  27795  scutbdaylt  27881  expsgt0  28433  tghilberti2  28664  brbtwn2  28938  axcontlem4  29000  axcontlem8  29004  clwlkl1loop  29819  clwwlknonex2lem2  30140  clwlknon2num  30400  numclwlk1lem2  30402  chscllem4  31672  orngmul  33298  measxun2  34174  measun  34175  mbfmco2  34230  probun  34384  satfv1fvfmla1  35391  cgrcomim  35953  cgrcoml  35960  cgrcomr  35961  cgrdegen  35968  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  btwnouttr  35988  btwnexch  35989  btwndiff  35991  lineid  36047  idinside  36048  btwnconn1lem7  36057  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem12  36062  btwnconn1lem14  36064  btwnconn3  36067  midofsegid  36068  segcon2  36069  brsegle2  36073  btwnoutside  36089  outsideoftr  36093  outsideofeu  36095  linethru  36117  cnres2  37723  heibor  37781  lsmsat  38964  lkrlsp  39058  lkrlsp2  39059  lkrlsp3  39060  latm4  39189  omlspjN  39217  hlatj4  39330  4noncolr3  39410  4noncolr2  39411  4noncolr1  39412  athgt  39413  3dimlem3a  39417  3dimlem4a  39420  3dimlem4  39421  3dimlem4OLDN  39422  3dim3  39426  1cvratex  39430  hlatexch4  39438  3atlem4  39443  atcvrlln2  39476  atcvrlln  39477  lplnnlelln  39500  lvoli2  39538  lvolnlelln  39541  lvolnlelpln  39542  4atlem11b  39565  4atlem12b  39568  2lplnja  39576  2lplnj  39577  dalemyeo  39589  dath2  39694  lncvrat  39739  cdlemblem  39750  cdlemb  39751  elpaddri  39759  padd4N  39797  llnmod2i2  39820  llnexchb2  39826  dalawlem1  39828  dalawlem2  39829  pclfinN  39857  osumcllem6N  39918  pexmidlem3N  39929  lhp2lt  39958  lhp2at0  39989  lhp2atnle  39990  lhp2atne  39991  lhp2at0nle  39992  lhp2at0ne  39993  lhpelim  39994  lhpmod2i2  39995  lhpmod6i1  39996  lhple  39999  lhpat  40000  lhpat3  40003  ltrncoelN  40100  ltrncoat  40101  ltrncnv  40103  trlat  40126  trl0  40127  ltrnnidn  40131  trlnid  40136  cdlemd7  40161  cdleme0b  40169  cdleme0c  40170  cdleme0fN  40175  cdleme02N  40179  cdleme0ex1N  40180  cdleme0ex2N  40181  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme8  40207  cdleme11a  40217  cdleme17c  40245  cdleme22gb  40251  cdlemeda  40255  cdleme20k  40276  cdleme21a  40282  cdleme21d  40287  cdleme22f2  40304  cdleme22g  40305  cdleme23a  40306  cdleme23b  40307  cdleme23c  40308  cdleme24  40309  cdleme28  40330  cdlemefrs32fva1  40358  cdlemefr32sn2aw  40361  cdlemefs32sn1aw  40371  cdleme41sn3a  40390  cdleme32fva  40394  cdleme32fva1  40395  cdleme35a  40405  cdleme35b  40407  cdleme35c  40408  cdleme35f  40411  cdleme39a  40422  cdleme42a  40428  cdleme42c  40429  cdleme42b  40435  cdleme42e  40436  cdleme42f  40437  cdleme42g  40438  cdleme42h  40439  cdleme43bN  40447  cdleme46f2g2  40450  cdleme17d2  40452  cdleme17d4  40454  cdleme48fv  40456  cdleme48fvg  40457  cdleme4gfv  40464  cdlemeg46c  40470  cdlemeg46nlpq  40474  cdlemeg46gfre  40489  cdleme48d  40492  cdlemeg49lebilem  40496  cdleme50trn2  40508  cdleme50ltrn  40514  cdleme  40517  cdlemf1  40518  cdlemf  40520  trlord  40526  ltrniotacnvval  40539  ltrniotavalbN  40541  cdlemg1cex  40545  cdlemg2dN  40547  cdlemg2ce  40549  cdlemg2fvlem  40551  cdlemg2idN  40553  cdlemg2kq  40559  cdlemg2l  40560  cdlemg2m  40561  cdlemg4b2  40567  cdlemg7fvN  40581  cdlemg8a  40584  cdlemg10bALTN  40593  cdlemg11aq  40595  cdlemg12d  40603  cdlemg13a  40608  cdlemg13  40609  cdlemg14f  40610  cdlemg14g  40611  cdlemg17a  40618  cdlemg17b  40619  cdlemg27a  40649  cdlemg31b0N  40651  cdlemg31a  40654  cdlemg31b  40655  cdlemg31c  40656  ltrnco  40676  trlcoabs  40678  trlcoabs2N  40679  trlcocnvat  40681  trlconid  40682  trlcolem  40683  trlcone  40685  cdlemg42  40686  cdlemg43  40687  cdlemg46  40692  cdlemg47  40693  tendoeq1  40721  tendoco2  40725  tendoplco2  40736  tendopltp  40737  cdlemh1  40772  cdlemh2  40773  cdlemi1  40775  cdlemi  40777  cdlemk1  40788  cdlemk2  40789  cdlemk3  40790  cdlemk4  40791  cdlemk8  40795  cdlemk9  40796  cdlemk9bN  40797  cdlemk31  40853  cdlemk32  40854  cdlemk28-3  40865  cdlemk19u  40927  cdlemk56w  40930  tendoex  40932  erngdvlem4  40948  erngdvlem4-rN  40956  dia11N  41005  dib11N  41117  cdlemn6  41159  cdlemn7  41160  cdlemn8  41161  cdlemn9  41162  dihordlem6  41170  dihordlem7  41171  dihord1  41175  dihord2a  41176  dihord2b  41177  dihord2pre  41182  dihord2pre2  41183  dihlsscpre  41191  dihvalcq2  41204  dihopelvalcpre  41205  dihord4  41215  dihord6b  41217  dihmeetlem1N  41247  dihglblem3N  41252  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetcN  41259  dihmeetbclemN  41261  dihmeetlem4preN  41263  dihjatc1  41268  dihjatc2N  41269  dihjatc3  41270  dihmeetlem9N  41272  dihmeetlem13N  41276  dihmeetlem20N  41283  dih1dimatlem0  41285  mapdpglem24  41661  mapdpglem32  41662  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  mapdh9aOLDN  41747  hdmap14lem6  41830  nnadddir  42259  sn-addlid  42380  mzpsubst  42704  pellexlem5  42789  pellex  42791  pell14qrexpclnn0  42822  pellfundex  42842  qirropth  42864  monotuz  42898  congtr  42922  congmul  42924  congsub  42927  mzpcong  42929  fzmaxdif  42938  jm2.15nn0  42960  idomsubgmo  43154  iunrelexpmin1  43670  iunrelexpmin2  43674  trclimalb2  43688  mnringmulrcld  44197  fourierdlem42  46070  fourierdlem48  46075  fourierdlem80  46107  smfaddlem1  46684  prmdvdsfmtnof1lem1  47458  uhgrimisgrgric  47783  uspgropssxp  47867  lidldomn1  47954  rngccatidALTV  47995  coe1sclmulval  48114  lincdifsn  48153  seposep  48605  iscnrm3rlem8  48627  iscnrm3llem2  48630