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  7119  f1oiso2  7286  fpr3g  8215  omeulem2  8498  uniinqs  8721  unxpdomlem3  9142  gruina  10706  dedekind  11273  addlid  11293  subaddmulsub  11577  dmdcan  11828  xaddass  13145  xaddass2  13146  xlt2add  13156  xmulasslem3  13182  xadddi2  13193  xadddi2r  13194  expaddzlem  14009  expaddz  14010  expmulz  14012  expdiv  14017  expmordi  14071  modexp  14142  pfxeq  14600  ccatopth2  14621  swrdco  14741  o1add  15518  o1mul  15519  o1sub  15520  fsumsplitsnun  15659  ntrivcvgmul  15806  prmexpb  16627  pcpremul  16752  pcdiv  16761  pcqmul  16762  pcqdiv  16766  4sqlem12  16865  f1ocpbllem  17425  ercpbl  17450  erlecpbl  17451  latjlej12  18358  latmlem12  18374  latj4  18392  latj4rot  18393  gsumsgrpccat  18745  gsmsymgreqlem2  19341  symgsssg  19377  symgfisg  19378  mndodcong  19452  cmn4  19711  ablsub4  19720  abladdsub4  19721  lsm4  19770  abvdom  20743  abvres  20744  abvtrivd  20745  orngmul  20778  lspsnvs  21049  lspsneu  21058  lspfixed  21063  lspexch  21064  lsmcv  21076  lspsolvlem  21077  ring2idlqus1  21254  coe1sclmulfv  22195  matvscacell  22349  m1detdiag  22510  cramerimplem3  22598  cnprest  23202  hausnei2  23266  isreg2  23290  cmpcld  23315  llyrest  23398  nllyrest  23399  elptr  23486  basqtop  23624  hausflimlem  23892  tmdgsum  24008  utop2nei  24163  trcfilu  24206  ssblps  24335  ssbl  24336  prdsxmslem2  24442  tgqioo  24713  metnrm  24776  bndth  24882  ncvspi  25081  ncvs1  25082  cph2ass  25138  lmmbr2  25184  iscau3  25203  bcthlem5  25253  ovolunlem2  25424  dvres2  25838  dvfsumlem2  25958  dvfsumlem2OLD  25959  plyadd  26147  plymul  26148  coeeu  26155  coemullem  26180  aalioulem4  26268  mulcxp  26619  cxplea  26630  cxple2  26631  cxplt2  26632  cxpcn3lem  26682  angcan  26737  ang180lem5  26748  divsqrtsumlem  26915  logexprlim  27161  dchrvmasumlema  27436  dchrisum0lema  27450  logdivsum  27469  log2sumbnd  27480  abvcxp  27551  padicabv  27566  nolesgn2ores  27609  nosupres  27644  nosupbnd1lem1  27645  nosupbnd1lem2  27646  nosupbnd1lem4  27648  nosupbnd1lem5  27649  nosupbnd1lem6  27650  noinffv  27658  noinfres  27659  noinfbnd1lem1  27660  noinfbnd1lem2  27661  noinfbnd1lem4  27663  noinfbnd1lem6  27665  nosupinfsep  27669  scutbdaylt  27757  expsgt0  28358  tghilberti2  28614  brbtwn2  28881  axcontlem4  28943  axcontlem8  28947  clwlkl1loop  29759  clwwlknonex2lem2  30083  clwlknon2num  30343  numclwlk1lem2  30345  chscllem4  31615  measxun2  34218  measun  34219  mbfmco2  34273  probun  34427  satfv1fvfmla1  35455  cgrcomim  36022  cgrcoml  36029  cgrcomr  36030  cgrdegen  36037  btwnintr  36052  btwnexch3  36053  btwnouttr2  36055  btwnouttr  36057  btwnexch  36058  btwndiff  36060  lineid  36116  idinside  36117  btwnconn1lem7  36126  btwnconn1lem8  36127  btwnconn1lem9  36128  btwnconn1lem12  36131  btwnconn1lem14  36133  btwnconn3  36136  midofsegid  36137  segcon2  36138  brsegle2  36142  btwnoutside  36158  outsideoftr  36162  outsideofeu  36164  linethru  36186  cnres2  37802  heibor  37860  lsmsat  39046  lkrlsp  39140  lkrlsp2  39141  lkrlsp3  39142  latm4  39271  omlspjN  39299  hlatj4  39412  4noncolr3  39491  4noncolr2  39492  4noncolr1  39493  athgt  39494  3dimlem3a  39498  3dimlem4a  39501  3dimlem4  39502  3dimlem4OLDN  39503  3dim3  39507  1cvratex  39511  hlatexch4  39519  3atlem4  39524  atcvrlln2  39557  atcvrlln  39558  lplnnlelln  39581  lvoli2  39619  lvolnlelln  39622  lvolnlelpln  39623  4atlem11b  39646  4atlem12b  39649  2lplnja  39657  2lplnj  39658  dalemyeo  39670  dath2  39775  lncvrat  39820  cdlemblem  39831  cdlemb  39832  elpaddri  39840  padd4N  39878  llnmod2i2  39901  llnexchb2  39907  dalawlem1  39909  dalawlem2  39910  pclfinN  39938  osumcllem6N  39999  pexmidlem3N  40010  lhp2lt  40039  lhp2at0  40070  lhp2atnle  40071  lhp2atne  40072  lhp2at0nle  40073  lhp2at0ne  40074  lhpelim  40075  lhpmod2i2  40076  lhpmod6i1  40077  lhple  40080  lhpat  40081  lhpat3  40084  ltrncoelN  40181  ltrncoat  40182  ltrncnv  40184  trlat  40207  trl0  40208  ltrnnidn  40212  trlnid  40217  cdlemd7  40242  cdleme0b  40250  cdleme0c  40251  cdleme0fN  40256  cdleme02N  40260  cdleme0ex1N  40261  cdleme0ex2N  40262  cdleme7aa  40280  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme8  40288  cdleme11a  40298  cdleme17c  40326  cdleme22gb  40332  cdlemeda  40336  cdleme20k  40357  cdleme21a  40363  cdleme21d  40368  cdleme22f2  40385  cdleme22g  40386  cdleme23a  40387  cdleme23b  40388  cdleme23c  40389  cdleme24  40390  cdleme28  40411  cdlemefrs32fva1  40439  cdlemefr32sn2aw  40442  cdlemefs32sn1aw  40452  cdleme41sn3a  40471  cdleme32fva  40475  cdleme32fva1  40476  cdleme35a  40486  cdleme35b  40488  cdleme35c  40489  cdleme35f  40492  cdleme39a  40503  cdleme42a  40509  cdleme42c  40510  cdleme42b  40516  cdleme42e  40517  cdleme42f  40518  cdleme42g  40519  cdleme42h  40520  cdleme43bN  40528  cdleme46f2g2  40531  cdleme17d2  40533  cdleme17d4  40535  cdleme48fv  40537  cdleme48fvg  40538  cdleme4gfv  40545  cdlemeg46c  40551  cdlemeg46nlpq  40555  cdlemeg46gfre  40570  cdleme48d  40573  cdlemeg49lebilem  40577  cdleme50trn2  40589  cdleme50ltrn  40595  cdleme  40598  cdlemf1  40599  cdlemf  40601  trlord  40607  ltrniotacnvval  40620  ltrniotavalbN  40622  cdlemg1cex  40626  cdlemg2dN  40628  cdlemg2ce  40630  cdlemg2fvlem  40632  cdlemg2idN  40634  cdlemg2kq  40640  cdlemg2l  40641  cdlemg2m  40642  cdlemg4b2  40648  cdlemg7fvN  40662  cdlemg8a  40665  cdlemg10bALTN  40674  cdlemg11aq  40676  cdlemg12d  40684  cdlemg13a  40689  cdlemg13  40690  cdlemg14f  40691  cdlemg14g  40692  cdlemg17a  40699  cdlemg17b  40700  cdlemg27a  40730  cdlemg31b0N  40732  cdlemg31a  40735  cdlemg31b  40736  cdlemg31c  40737  ltrnco  40757  trlcoabs  40759  trlcoabs2N  40760  trlcocnvat  40762  trlconid  40763  trlcolem  40764  trlcone  40766  cdlemg42  40767  cdlemg43  40768  cdlemg46  40773  cdlemg47  40774  tendoeq1  40802  tendoco2  40806  tendoplco2  40817  tendopltp  40818  cdlemh1  40853  cdlemh2  40854  cdlemi1  40856  cdlemi  40858  cdlemk1  40869  cdlemk2  40870  cdlemk3  40871  cdlemk4  40872  cdlemk8  40876  cdlemk9  40877  cdlemk9bN  40878  cdlemk31  40934  cdlemk32  40935  cdlemk28-3  40946  cdlemk19u  41008  cdlemk56w  41011  tendoex  41013  erngdvlem4  41029  erngdvlem4-rN  41037  dia11N  41086  dib11N  41198  cdlemn6  41240  cdlemn7  41241  cdlemn8  41242  cdlemn9  41243  dihordlem6  41251  dihordlem7  41252  dihord1  41256  dihord2a  41257  dihord2b  41258  dihord2pre  41263  dihord2pre2  41264  dihlsscpre  41272  dihvalcq2  41285  dihopelvalcpre  41286  dihord4  41296  dihord6b  41298  dihmeetlem1N  41328  dihglblem3N  41333  dihmeetlem2N  41337  dihglbcpreN  41338  dihmeetcN  41340  dihmeetbclemN  41342  dihmeetlem4preN  41344  dihjatc1  41349  dihjatc2N  41350  dihjatc3  41351  dihmeetlem9N  41353  dihmeetlem13N  41357  dihmeetlem20N  41364  dih1dimatlem0  41366  mapdpglem24  41742  mapdpglem32  41743  baerlem3lem2  41748  baerlem5alem2  41749  baerlem5blem2  41750  mapdh9aOLDN  41828  hdmap14lem6  41911  nnadddir  42302  sn-addlid  42436  mzpsubst  42780  pellexlem5  42865  pellex  42867  pell14qrexpclnn0  42898  pellfundex  42918  qirropth  42940  monotuz  42973  congtr  42997  congmul  42999  congsub  43002  mzpcong  43004  fzmaxdif  43013  jm2.15nn0  43035  idomsubgmo  43225  iunrelexpmin1  43740  iunrelexpmin2  43744  trclimalb2  43758  mnringmulrcld  44260  fourierdlem42  46186  fourierdlem48  46191  fourierdlem80  46223  smfaddlem1  46800  prmdvdsfmtnof1lem1  47614  uhgrimisgrgric  47961  uspgropssxp  48174  lidldomn1  48261  rngccatidALTV  48302  coe1sclmulval  48416  lincdifsn  48455  seposep  48956  iscnrm3rlem8  48977  iscnrm3llem2  48980