Theorem simp2l 1200

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

This theorem is referenced by:  simp12l  1287  simp22l  1293  simp32l  1299  fsnunf  7125  f1oiso2  7292  fpr3g  8221  omeulem2  8504  uniinqs  8727  unxpdomlem3  9149  gruina  10716  dedekind  11283  addlid  11303  subaddmulsub  11587  dmdcan  11838  xaddass  13150  xaddass2  13151  xlt2add  13161  xmulasslem3  13187  xadddi2  13198  xadddi2r  13199  expaddzlem  14014  expaddz  14015  expmulz  14017  expdiv  14022  expmordi  14076  modexp  14147  pfxeq  14605  ccatopth2  14626  swrdco  14746  o1add  15523  o1mul  15524  o1sub  15525  fsumsplitsnun  15664  ntrivcvgmul  15811  prmexpb  16632  pcpremul  16757  pcdiv  16766  pcqmul  16767  pcqdiv  16771  4sqlem12  16870  f1ocpbllem  17430  ercpbl  17455  erlecpbl  17456  latjlej12  18363  latmlem12  18379  latj4  18397  latj4rot  18398  gsumsgrpccat  18750  gsmsymgreqlem2  19345  symgsssg  19381  symgfisg  19382  mndodcong  19456  cmn4  19715  ablsub4  19724  abladdsub4  19725  lsm4  19774  abvdom  20747  abvres  20748  abvtrivd  20749  orngmul  20782  lspsnvs  21053  lspsneu  21062  lspfixed  21067  lspexch  21068  lsmcv  21080  lspsolvlem  21081  ring2idlqus1  21258  coe1sclmulfv  22198  matvscacell  22352  m1detdiag  22513  cramerimplem3  22601  cnprest  23205  hausnei2  23269  isreg2  23293  cmpcld  23318  llyrest  23401  nllyrest  23402  elptr  23489  basqtop  23627  hausflimlem  23895  tmdgsum  24011  utop2nei  24166  trcfilu  24209  ssblps  24338  ssbl  24339  prdsxmslem2  24445  tgqioo  24716  metnrm  24779  bndth  24885  ncvspi  25084  ncvs1  25085  cph2ass  25141  lmmbr2  25187  iscau3  25206  bcthlem5  25256  ovolunlem2  25427  dvres2  25841  dvfsumlem2  25961  dvfsumlem2OLD  25962  plyadd  26150  plymul  26151  coeeu  26158  coemullem  26183  aalioulem4  26271  mulcxp  26622  cxplea  26633  cxple2  26634  cxplt2  26635  cxpcn3lem  26685  angcan  26740  ang180lem5  26751  divsqrtsumlem  26918  logexprlim  27164  dchrvmasumlema  27439  dchrisum0lema  27453  logdivsum  27472  log2sumbnd  27483  abvcxp  27554  padicabv  27569  nolesgn2ores  27612  nosupres  27647  nosupbnd1lem1  27648  nosupbnd1lem2  27649  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd1lem6  27653  noinffv  27661  noinfres  27662  noinfbnd1lem1  27663  noinfbnd1lem2  27664  noinfbnd1lem4  27666  noinfbnd1lem6  27668  nosupinfsep  27672  scutbdaylt  27760  expsgt0  28361  tghilberti2  28617  brbtwn2  28885  axcontlem4  28947  axcontlem8  28951  clwlkl1loop  29763  clwwlknonex2lem2  30090  clwlknon2num  30350  numclwlk1lem2  30352  chscllem4  31622  measxun2  34244  measun  34245  mbfmco2  34299  probun  34453  satfv1fvfmla1  35488  cgrcomim  36054  cgrcoml  36061  cgrcomr  36062  cgrdegen  36069  btwnintr  36084  btwnexch3  36085  btwnouttr2  36087  btwnouttr  36089  btwnexch  36090  btwndiff  36092  lineid  36148  idinside  36149  btwnconn1lem7  36158  btwnconn1lem8  36159  btwnconn1lem9  36160  btwnconn1lem12  36163  btwnconn1lem14  36165  btwnconn3  36168  midofsegid  36169  segcon2  36170  brsegle2  36174  btwnoutside  36190  outsideoftr  36194  outsideofeu  36196  linethru  36218  cnres2  37823  heibor  37881  lsmsat  39127  lkrlsp  39221  lkrlsp2  39222  lkrlsp3  39223  latm4  39352  omlspjN  39380  hlatj4  39493  4noncolr3  39572  4noncolr2  39573  4noncolr1  39574  athgt  39575  3dimlem3a  39579  3dimlem4a  39582  3dimlem4  39583  3dimlem4OLDN  39584  3dim3  39588  1cvratex  39592  hlatexch4  39600  3atlem4  39605  atcvrlln2  39638  atcvrlln  39639  lplnnlelln  39662  lvoli2  39700  lvolnlelln  39703  lvolnlelpln  39704  4atlem11b  39727  4atlem12b  39730  2lplnja  39738  2lplnj  39739  dalemyeo  39751  dath2  39856  lncvrat  39901  cdlemblem  39912  cdlemb  39913  elpaddri  39921  padd4N  39959  llnmod2i2  39982  llnexchb2  39988  dalawlem1  39990  dalawlem2  39991  pclfinN  40019  osumcllem6N  40080  pexmidlem3N  40091  lhp2lt  40120  lhp2at0  40151  lhp2atnle  40152  lhp2atne  40153  lhp2at0nle  40154  lhp2at0ne  40155  lhpelim  40156  lhpmod2i2  40157  lhpmod6i1  40158  lhple  40161  lhpat  40162  lhpat3  40165  ltrncoelN  40262  ltrncoat  40263  ltrncnv  40265  trlat  40288  trl0  40289  ltrnnidn  40293  trlnid  40298  cdlemd7  40323  cdleme0b  40331  cdleme0c  40332  cdleme0fN  40337  cdleme02N  40341  cdleme0ex1N  40342  cdleme0ex2N  40343  cdleme7aa  40361  cdleme7c  40364  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme7  40368  cdleme8  40369  cdleme11a  40379  cdleme17c  40407  cdleme22gb  40413  cdlemeda  40417  cdleme20k  40438  cdleme21a  40444  cdleme21d  40449  cdleme22f2  40466  cdleme22g  40467  cdleme23a  40468  cdleme23b  40469  cdleme23c  40470  cdleme24  40471  cdleme28  40492  cdlemefrs32fva1  40520  cdlemefr32sn2aw  40523  cdlemefs32sn1aw  40533  cdleme41sn3a  40552  cdleme32fva  40556  cdleme32fva1  40557  cdleme35a  40567  cdleme35b  40569  cdleme35c  40570  cdleme35f  40573  cdleme39a  40584  cdleme42a  40590  cdleme42c  40591  cdleme42b  40597  cdleme42e  40598  cdleme42f  40599  cdleme42g  40600  cdleme42h  40601  cdleme43bN  40609  cdleme46f2g2  40612  cdleme17d2  40614  cdleme17d4  40616  cdleme48fv  40618  cdleme48fvg  40619  cdleme4gfv  40626  cdlemeg46c  40632  cdlemeg46nlpq  40636  cdlemeg46gfre  40651  cdleme48d  40654  cdlemeg49lebilem  40658  cdleme50trn2  40670  cdleme50ltrn  40676  cdleme  40679  cdlemf1  40680  cdlemf  40682  trlord  40688  ltrniotacnvval  40701  ltrniotavalbN  40703  cdlemg1cex  40707  cdlemg2dN  40709  cdlemg2ce  40711  cdlemg2fvlem  40713  cdlemg2idN  40715  cdlemg2kq  40721  cdlemg2l  40722  cdlemg2m  40723  cdlemg4b2  40729  cdlemg7fvN  40743  cdlemg8a  40746  cdlemg10bALTN  40755  cdlemg11aq  40757  cdlemg12d  40765  cdlemg13a  40770  cdlemg13  40771  cdlemg14f  40772  cdlemg14g  40773  cdlemg17a  40780  cdlemg17b  40781  cdlemg27a  40811  cdlemg31b0N  40813  cdlemg31a  40816  cdlemg31b  40817  cdlemg31c  40818  ltrnco  40838  trlcoabs  40840  trlcoabs2N  40841  trlcocnvat  40843  trlconid  40844  trlcolem  40845  trlcone  40847  cdlemg42  40848  cdlemg43  40849  cdlemg46  40854  cdlemg47  40855  tendoeq1  40883  tendoco2  40887  tendoplco2  40898  tendopltp  40899  cdlemh1  40934  cdlemh2  40935  cdlemi1  40937  cdlemi  40939  cdlemk1  40950  cdlemk2  40951  cdlemk3  40952  cdlemk4  40953  cdlemk8  40957  cdlemk9  40958  cdlemk9bN  40959  cdlemk31  41015  cdlemk32  41016  cdlemk28-3  41027  cdlemk19u  41089  cdlemk56w  41092  tendoex  41094  erngdvlem4  41110  erngdvlem4-rN  41118  dia11N  41167  dib11N  41279  cdlemn6  41321  cdlemn7  41322  cdlemn8  41323  cdlemn9  41324  dihordlem6  41332  dihordlem7  41333  dihord1  41337  dihord2a  41338  dihord2b  41339  dihord2pre  41344  dihord2pre2  41345  dihlsscpre  41353  dihvalcq2  41366  dihopelvalcpre  41367  dihord4  41377  dihord6b  41379  dihmeetlem1N  41409  dihglblem3N  41414  dihmeetlem2N  41418  dihglbcpreN  41419  dihmeetcN  41421  dihmeetbclemN  41423  dihmeetlem4preN  41425  dihjatc1  41430  dihjatc2N  41431  dihjatc3  41432  dihmeetlem9N  41434  dihmeetlem13N  41438  dihmeetlem20N  41445  dih1dimatlem0  41447  mapdpglem24  41823  mapdpglem32  41824  baerlem3lem2  41829  baerlem5alem2  41830  baerlem5blem2  41831  mapdh9aOLDN  41909  hdmap14lem6  41992  nnadddir  42388  sn-addlid  42522  mzpsubst  42865  pellexlem5  42950  pellex  42952  pell14qrexpclnn0  42983  pellfundex  43003  qirropth  43025  monotuz  43058  congtr  43082  congmul  43084  congsub  43087  mzpcong  43089  fzmaxdif  43098  jm2.15nn0  43120  idomsubgmo  43310  iunrelexpmin1  43825  iunrelexpmin2  43829  trclimalb2  43843  mnringmulrcld  44345  fourierdlem42  46271  fourierdlem48  46276  fourierdlem80  46308  smfaddlem1  46885  prmdvdsfmtnof1lem1  47708  uhgrimisgrgric  48055  uspgropssxp  48268  lidldomn1  48355  rngccatidALTV  48396  coe1sclmulval  48510  lincdifsn  48549  seposep  49050  iscnrm3rlem8  49071  iscnrm3llem2  49074