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  7162  f1oiso2  7330  fpr3g  8267  omeulem2  8550  uniinqs  8773  unxpdomlem3  9206  gruina  10778  dedekind  11344  addlid  11364  subaddmulsub  11648  dmdcan  11899  xaddass  13216  xaddass2  13217  xlt2add  13227  xmulasslem3  13253  xadddi2  13264  xadddi2r  13265  expaddzlem  14077  expaddz  14078  expmulz  14080  expdiv  14085  expmordi  14139  modexp  14210  pfxeq  14668  ccatopth2  14689  swrdco  14810  o1add  15587  o1mul  15588  o1sub  15589  fsumsplitsnun  15728  ntrivcvgmul  15875  prmexpb  16696  pcpremul  16821  pcdiv  16830  pcqmul  16831  pcqdiv  16835  4sqlem12  16934  f1ocpbllem  17494  ercpbl  17519  erlecpbl  17520  latjlej12  18421  latmlem12  18437  latj4  18455  latj4rot  18456  gsumsgrpccat  18774  gsmsymgreqlem2  19368  symgsssg  19404  symgfisg  19405  mndodcong  19479  cmn4  19738  ablsub4  19747  abladdsub4  19748  lsm4  19797  abvdom  20746  abvres  20747  abvtrivd  20748  lspsnvs  21031  lspsneu  21040  lspfixed  21045  lspexch  21046  lsmcv  21058  lspsolvlem  21059  ring2idlqus1  21236  coe1sclmulfv  22176  matvscacell  22330  m1detdiag  22491  cramerimplem3  22579  cnprest  23183  hausnei2  23247  isreg2  23271  cmpcld  23296  llyrest  23379  nllyrest  23380  elptr  23467  basqtop  23605  hausflimlem  23873  tmdgsum  23989  utop2nei  24145  trcfilu  24188  ssblps  24317  ssbl  24318  prdsxmslem2  24424  tgqioo  24695  metnrm  24758  bndth  24864  ncvspi  25063  ncvs1  25064  cph2ass  25120  lmmbr2  25166  iscau3  25185  bcthlem5  25235  ovolunlem2  25406  dvres2  25820  dvfsumlem2  25940  dvfsumlem2OLD  25941  plyadd  26129  plymul  26130  coeeu  26137  coemullem  26162  aalioulem4  26250  mulcxp  26601  cxplea  26612  cxple2  26613  cxplt2  26614  cxpcn3lem  26664  angcan  26719  ang180lem5  26730  divsqrtsumlem  26897  logexprlim  27143  dchrvmasumlema  27418  dchrisum0lema  27432  logdivsum  27451  log2sumbnd  27462  abvcxp  27533  padicabv  27548  nolesgn2ores  27591  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1lem2  27628  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd1lem6  27632  noinffv  27640  noinfres  27641  noinfbnd1lem1  27642  noinfbnd1lem2  27643  noinfbnd1lem4  27645  noinfbnd1lem6  27647  nosupinfsep  27651  scutbdaylt  27737  expsgt0  28329  tghilberti2  28572  brbtwn2  28839  axcontlem4  28901  axcontlem8  28905  clwlkl1loop  29720  clwwlknonex2lem2  30044  clwlknon2num  30304  numclwlk1lem2  30306  chscllem4  31576  orngmul  33288  measxun2  34207  measun  34208  mbfmco2  34263  probun  34417  satfv1fvfmla1  35417  cgrcomim  35984  cgrcoml  35991  cgrcomr  35992  cgrdegen  35999  btwnintr  36014  btwnexch3  36015  btwnouttr2  36017  btwnouttr  36019  btwnexch  36020  btwndiff  36022  lineid  36078  idinside  36079  btwnconn1lem7  36088  btwnconn1lem8  36089  btwnconn1lem9  36090  btwnconn1lem12  36093  btwnconn1lem14  36095  btwnconn3  36098  midofsegid  36099  segcon2  36100  brsegle2  36104  btwnoutside  36120  outsideoftr  36124  outsideofeu  36126  linethru  36148  cnres2  37764  heibor  37822  lsmsat  39008  lkrlsp  39102  lkrlsp2  39103  lkrlsp3  39104  latm4  39233  omlspjN  39261  hlatj4  39374  4noncolr3  39454  4noncolr2  39455  4noncolr1  39456  athgt  39457  3dimlem3a  39461  3dimlem4a  39464  3dimlem4  39465  3dimlem4OLDN  39466  3dim3  39470  1cvratex  39474  hlatexch4  39482  3atlem4  39487  atcvrlln2  39520  atcvrlln  39521  lplnnlelln  39544  lvoli2  39582  lvolnlelln  39585  lvolnlelpln  39586  4atlem11b  39609  4atlem12b  39612  2lplnja  39620  2lplnj  39621  dalemyeo  39633  dath2  39738  lncvrat  39783  cdlemblem  39794  cdlemb  39795  elpaddri  39803  padd4N  39841  llnmod2i2  39864  llnexchb2  39870  dalawlem1  39872  dalawlem2  39873  pclfinN  39901  osumcllem6N  39962  pexmidlem3N  39973  lhp2lt  40002  lhp2at0  40033  lhp2atnle  40034  lhp2atne  40035  lhp2at0nle  40036  lhp2at0ne  40037  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  lhple  40043  lhpat  40044  lhpat3  40047  ltrncoelN  40144  ltrncoat  40145  ltrncnv  40147  trlat  40170  trl0  40171  ltrnnidn  40175  trlnid  40180  cdlemd7  40205  cdleme0b  40213  cdleme0c  40214  cdleme0fN  40219  cdleme02N  40223  cdleme0ex1N  40224  cdleme0ex2N  40225  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme8  40251  cdleme11a  40261  cdleme17c  40289  cdleme22gb  40295  cdlemeda  40299  cdleme20k  40320  cdleme21a  40326  cdleme21d  40331  cdleme22f2  40348  cdleme22g  40349  cdleme23a  40350  cdleme23b  40351  cdleme23c  40352  cdleme24  40353  cdleme28  40374  cdlemefrs32fva1  40402  cdlemefr32sn2aw  40405  cdlemefs32sn1aw  40415  cdleme41sn3a  40434  cdleme32fva  40438  cdleme32fva1  40439  cdleme35a  40449  cdleme35b  40451  cdleme35c  40452  cdleme35f  40455  cdleme39a  40466  cdleme42a  40472  cdleme42c  40473  cdleme42b  40479  cdleme42e  40480  cdleme42f  40481  cdleme42g  40482  cdleme42h  40483  cdleme43bN  40491  cdleme46f2g2  40494  cdleme17d2  40496  cdleme17d4  40498  cdleme48fv  40500  cdleme48fvg  40501  cdleme4gfv  40508  cdlemeg46c  40514  cdlemeg46nlpq  40518  cdlemeg46gfre  40533  cdleme48d  40536  cdlemeg49lebilem  40540  cdleme50trn2  40552  cdleme50ltrn  40558  cdleme  40561  cdlemf1  40562  cdlemf  40564  trlord  40570  ltrniotacnvval  40583  ltrniotavalbN  40585  cdlemg1cex  40589  cdlemg2dN  40591  cdlemg2ce  40593  cdlemg2fvlem  40595  cdlemg2idN  40597  cdlemg2kq  40603  cdlemg2l  40604  cdlemg2m  40605  cdlemg4b2  40611  cdlemg7fvN  40625  cdlemg8a  40628  cdlemg10bALTN  40637  cdlemg11aq  40639  cdlemg12d  40647  cdlemg13a  40652  cdlemg13  40653  cdlemg14f  40654  cdlemg14g  40655  cdlemg17a  40662  cdlemg17b  40663  cdlemg27a  40693  cdlemg31b0N  40695  cdlemg31a  40698  cdlemg31b  40699  cdlemg31c  40700  ltrnco  40720  trlcoabs  40722  trlcoabs2N  40723  trlcocnvat  40725  trlconid  40726  trlcolem  40727  trlcone  40729  cdlemg42  40730  cdlemg43  40731  cdlemg46  40736  cdlemg47  40737  tendoeq1  40765  tendoco2  40769  tendoplco2  40780  tendopltp  40781  cdlemh1  40816  cdlemh2  40817  cdlemi1  40819  cdlemi  40821  cdlemk1  40832  cdlemk2  40833  cdlemk3  40834  cdlemk4  40835  cdlemk8  40839  cdlemk9  40840  cdlemk9bN  40841  cdlemk31  40897  cdlemk32  40898  cdlemk28-3  40909  cdlemk19u  40971  cdlemk56w  40974  tendoex  40976  erngdvlem4  40992  erngdvlem4-rN  41000  dia11N  41049  dib11N  41161  cdlemn6  41203  cdlemn7  41204  cdlemn8  41205  cdlemn9  41206  dihordlem6  41214  dihordlem7  41215  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord2pre  41226  dihord2pre2  41227  dihlsscpre  41235  dihvalcq2  41248  dihopelvalcpre  41249  dihord4  41259  dihord6b  41261  dihmeetlem1N  41291  dihglblem3N  41296  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetcN  41303  dihmeetbclemN  41305  dihmeetlem4preN  41307  dihjatc1  41312  dihjatc2N  41313  dihjatc3  41314  dihmeetlem9N  41316  dihmeetlem13N  41320  dihmeetlem20N  41327  dih1dimatlem0  41329  mapdpglem24  41705  mapdpglem32  41706  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  mapdh9aOLDN  41791  hdmap14lem6  41874  nnadddir  42265  sn-addlid  42399  mzpsubst  42743  pellexlem5  42828  pellex  42830  pell14qrexpclnn0  42861  pellfundex  42881  qirropth  42903  monotuz  42937  congtr  42961  congmul  42963  congsub  42966  mzpcong  42968  fzmaxdif  42977  jm2.15nn0  42999  idomsubgmo  43189  iunrelexpmin1  43704  iunrelexpmin2  43708  trclimalb2  43722  mnringmulrcld  44224  fourierdlem42  46154  fourierdlem48  46159  fourierdlem80  46191  smfaddlem1  46768  prmdvdsfmtnof1lem1  47589  uhgrimisgrgric  47935  uspgropssxp  48136  lidldomn1  48223  rngccatidALTV  48264  coe1sclmulval  48378  lincdifsn  48417  seposep  48918  iscnrm3rlem8  48939  iscnrm3llem2  48942