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 1135	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  1287  simp22l  1293  simp32l  1299  fsnunf  7205  f1oiso2  7372  fpr3g  8310  omeulem2  8621  uniinqs  8837  unxpdomlem3  9288  gruina  10858  dedekind  11424  addlid  11444  subaddmulsub  11726  dmdcan  11977  xaddass  13291  xaddass2  13292  xlt2add  13302  xmulasslem3  13328  xadddi2  13339  xadddi2r  13340  expaddzlem  14146  expaddz  14147  expmulz  14149  expdiv  14154  expmordi  14207  modexp  14277  pfxeq  14734  ccatopth2  14755  swrdco  14876  o1add  15650  o1mul  15651  o1sub  15652  fsumsplitsnun  15791  ntrivcvgmul  15938  prmexpb  16756  pcpremul  16881  pcdiv  16890  pcqmul  16891  pcqdiv  16895  4sqlem12  16994  f1ocpbllem  17569  ercpbl  17594  erlecpbl  17595  latjlej12  18500  latmlem12  18516  latj4  18534  latj4rot  18535  gsumsgrpccat  18853  gsmsymgreqlem2  19449  symgsssg  19485  symgfisg  19486  mndodcong  19560  cmn4  19819  ablsub4  19828  abladdsub4  19829  lsm4  19878  abvdom  20831  abvres  20832  abvtrivd  20833  lspsnvs  21116  lspsneu  21125  lspfixed  21130  lspexch  21131  lsmcv  21143  lspsolvlem  21144  ring2idlqus1  21329  coe1sclmulfv  22286  matvscacell  22442  m1detdiag  22603  cramerimplem3  22691  cnprest  23297  hausnei2  23361  isreg2  23385  cmpcld  23410  llyrest  23493  nllyrest  23494  elptr  23581  basqtop  23719  hausflimlem  23987  tmdgsum  24103  utop2nei  24259  trcfilu  24303  ssblps  24432  ssbl  24433  prdsxmslem2  24542  tgqioo  24821  metnrm  24884  bndth  24990  ncvspi  25190  ncvs1  25191  cph2ass  25247  lmmbr2  25293  iscau3  25312  bcthlem5  25362  ovolunlem2  25533  dvres2  25947  dvfsumlem2  26067  dvfsumlem2OLD  26068  plyadd  26256  plymul  26257  coeeu  26264  coemullem  26289  aalioulem4  26377  mulcxp  26727  cxplea  26738  cxple2  26739  cxplt2  26740  cxpcn3lem  26790  angcan  26845  ang180lem5  26856  divsqrtsumlem  27023  logexprlim  27269  dchrvmasumlema  27544  dchrisum0lema  27558  logdivsum  27577  log2sumbnd  27588  abvcxp  27659  padicabv  27674  nolesgn2ores  27717  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem2  27754  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd1lem6  27758  noinffv  27766  noinfres  27767  noinfbnd1lem1  27768  noinfbnd1lem2  27769  noinfbnd1lem4  27771  noinfbnd1lem6  27773  nosupinfsep  27777  scutbdaylt  27863  expsgt0  28415  tghilberti2  28646  brbtwn2  28920  axcontlem4  28982  axcontlem8  28986  clwlkl1loop  29803  clwwlknonex2lem2  30127  clwlknon2num  30387  numclwlk1lem2  30389  chscllem4  31659  orngmul  33333  measxun2  34211  measun  34212  mbfmco2  34267  probun  34421  satfv1fvfmla1  35428  cgrcomim  35990  cgrcoml  35997  cgrcomr  35998  cgrdegen  36005  btwnintr  36020  btwnexch3  36021  btwnouttr2  36023  btwnouttr  36025  btwnexch  36026  btwndiff  36028  lineid  36084  idinside  36085  btwnconn1lem7  36094  btwnconn1lem8  36095  btwnconn1lem9  36096  btwnconn1lem12  36099  btwnconn1lem14  36101  btwnconn3  36104  midofsegid  36105  segcon2  36106  brsegle2  36110  btwnoutside  36126  outsideoftr  36130  outsideofeu  36132  linethru  36154  cnres2  37770  heibor  37828  lsmsat  39009  lkrlsp  39103  lkrlsp2  39104  lkrlsp3  39105  latm4  39234  omlspjN  39262  hlatj4  39375  4noncolr3  39455  4noncolr2  39456  4noncolr1  39457  athgt  39458  3dimlem3a  39462  3dimlem4a  39465  3dimlem4  39466  3dimlem4OLDN  39467  3dim3  39471  1cvratex  39475  hlatexch4  39483  3atlem4  39488  atcvrlln2  39521  atcvrlln  39522  lplnnlelln  39545  lvoli2  39583  lvolnlelln  39586  lvolnlelpln  39587  4atlem11b  39610  4atlem12b  39613  2lplnja  39621  2lplnj  39622  dalemyeo  39634  dath2  39739  lncvrat  39784  cdlemblem  39795  cdlemb  39796  elpaddri  39804  padd4N  39842  llnmod2i2  39865  llnexchb2  39871  dalawlem1  39873  dalawlem2  39874  pclfinN  39902  osumcllem6N  39963  pexmidlem3N  39974  lhp2lt  40003  lhp2at0  40034  lhp2atnle  40035  lhp2atne  40036  lhp2at0nle  40037  lhp2at0ne  40038  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  lhple  40044  lhpat  40045  lhpat3  40048  ltrncoelN  40145  ltrncoat  40146  ltrncnv  40148  trlat  40171  trl0  40172  ltrnnidn  40176  trlnid  40181  cdlemd7  40206  cdleme0b  40214  cdleme0c  40215  cdleme0fN  40220  cdleme02N  40224  cdleme0ex1N  40225  cdleme0ex2N  40226  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme8  40252  cdleme11a  40262  cdleme17c  40290  cdleme22gb  40296  cdlemeda  40300  cdleme20k  40321  cdleme21a  40327  cdleme21d  40332  cdleme22f2  40349  cdleme22g  40350  cdleme23a  40351  cdleme23b  40352  cdleme23c  40353  cdleme24  40354  cdleme28  40375  cdlemefrs32fva1  40403  cdlemefr32sn2aw  40406  cdlemefs32sn1aw  40416  cdleme41sn3a  40435  cdleme32fva  40439  cdleme32fva1  40440  cdleme35a  40450  cdleme35b  40452  cdleme35c  40453  cdleme35f  40456  cdleme39a  40467  cdleme42a  40473  cdleme42c  40474  cdleme42b  40480  cdleme42e  40481  cdleme42f  40482  cdleme42g  40483  cdleme42h  40484  cdleme43bN  40492  cdleme46f2g2  40495  cdleme17d2  40497  cdleme17d4  40499  cdleme48fv  40501  cdleme48fvg  40502  cdleme4gfv  40509  cdlemeg46c  40515  cdlemeg46nlpq  40519  cdlemeg46gfre  40534  cdleme48d  40537  cdlemeg49lebilem  40541  cdleme50trn2  40553  cdleme50ltrn  40559  cdleme  40562  cdlemf1  40563  cdlemf  40565  trlord  40571  ltrniotacnvval  40584  ltrniotavalbN  40586  cdlemg1cex  40590  cdlemg2dN  40592  cdlemg2ce  40594  cdlemg2fvlem  40596  cdlemg2idN  40598  cdlemg2kq  40604  cdlemg2l  40605  cdlemg2m  40606  cdlemg4b2  40612  cdlemg7fvN  40626  cdlemg8a  40629  cdlemg10bALTN  40638  cdlemg11aq  40640  cdlemg12d  40648  cdlemg13a  40653  cdlemg13  40654  cdlemg14f  40655  cdlemg14g  40656  cdlemg17a  40663  cdlemg17b  40664  cdlemg27a  40694  cdlemg31b0N  40696  cdlemg31a  40699  cdlemg31b  40700  cdlemg31c  40701  ltrnco  40721  trlcoabs  40723  trlcoabs2N  40724  trlcocnvat  40726  trlconid  40727  trlcolem  40728  trlcone  40730  cdlemg42  40731  cdlemg43  40732  cdlemg46  40737  cdlemg47  40738  tendoeq1  40766  tendoco2  40770  tendoplco2  40781  tendopltp  40782  cdlemh1  40817  cdlemh2  40818  cdlemi1  40820  cdlemi  40822  cdlemk1  40833  cdlemk2  40834  cdlemk3  40835  cdlemk4  40836  cdlemk8  40840  cdlemk9  40841  cdlemk9bN  40842  cdlemk31  40898  cdlemk32  40899  cdlemk28-3  40910  cdlemk19u  40972  cdlemk56w  40975  tendoex  40977  erngdvlem4  40993  erngdvlem4-rN  41001  dia11N  41050  dib11N  41162  cdlemn6  41204  cdlemn7  41205  cdlemn8  41206  cdlemn9  41207  dihordlem6  41215  dihordlem7  41216  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord2pre  41227  dihord2pre2  41228  dihlsscpre  41236  dihvalcq2  41249  dihopelvalcpre  41250  dihord4  41260  dihord6b  41262  dihmeetlem1N  41292  dihglblem3N  41297  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetcN  41304  dihmeetbclemN  41306  dihmeetlem4preN  41308  dihjatc1  41313  dihjatc2N  41314  dihjatc3  41315  dihmeetlem9N  41317  dihmeetlem13N  41321  dihmeetlem20N  41328  dih1dimatlem0  41330  mapdpglem24  41706  mapdpglem32  41707  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  mapdh9aOLDN  41792  hdmap14lem6  41875  nnadddir  42305  sn-addlid  42434  mzpsubst  42759  pellexlem5  42844  pellex  42846  pell14qrexpclnn0  42877  pellfundex  42897  qirropth  42919  monotuz  42953  congtr  42977  congmul  42979  congsub  42982  mzpcong  42984  fzmaxdif  42993  jm2.15nn0  43015  idomsubgmo  43205  iunrelexpmin1  43721  iunrelexpmin2  43725  trclimalb2  43739  mnringmulrcld  44247  fourierdlem42  46164  fourierdlem48  46169  fourierdlem80  46201  smfaddlem1  46778  prmdvdsfmtnof1lem1  47571  uhgrimisgrgric  47899  uspgropssxp  48060  lidldomn1  48147  rngccatidALTV  48188  coe1sclmulval  48302  lincdifsn  48341  seposep  48823  iscnrm3rlem8  48844  iscnrm3llem2  48847