Theorem simp2l 1198

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 483	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1133	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp12l  1285  simp22l  1291  simp32l  1297  fsnunf  7054  f1oiso2  7219  fpr3g  8092  omeulem2  8399  uniinqs  8569  unxpdomlem3  9007  gruina  10575  dedekind  11138  addid2  11158  subaddmulsub  11438  dmdcan  11685  xaddass  12982  xaddass2  12983  xlt2add  12993  xmulasslem3  13019  xadddi2  13030  xadddi2r  13031  expaddzlem  13824  expaddz  13825  expmulz  13827  expdiv  13832  expmordi  13883  modexp  13951  pfxeq  14407  ccatopth2  14428  swrdco  14548  o1add  15321  o1mul  15322  o1sub  15323  fsumsplitsnun  15465  ntrivcvgmul  15612  prmexpb  16423  pcpremul  16542  pcdiv  16551  pcqmul  16552  pcqdiv  16556  4sqlem12  16655  f1ocpbllem  17233  ercpbl  17258  erlecpbl  17259  latjlej12  18171  latmlem12  18187  latj4  18205  latj4rot  18206  gsumsgrpccat  18476  gsmsymgreqlem2  19037  symgsssg  19073  symgfisg  19074  mndodcong  19148  cmn4  19404  ablsub4  19412  abladdsub4  19413  lsm4  19459  abvdom  20096  abvres  20097  abvtrivd  20098  lspsnvs  20374  lspsneu  20383  lspfixed  20388  lspexch  20389  lsmcv  20401  lspsolvlem  20402  coe1sclmulfv  21452  matvscacell  21583  m1detdiag  21744  cramerimplem3  21832  cnprest  22438  hausnei2  22502  isreg2  22526  cmpcld  22551  llyrest  22634  nllyrest  22635  elptr  22722  basqtop  22860  hausflimlem  23128  tmdgsum  23244  utop2nei  23400  trcfilu  23444  ssblps  23573  ssbl  23574  prdsxmslem2  23683  tgqioo  23961  metnrm  24023  bndth  24119  ncvspi  24318  ncvs1  24319  cph2ass  24375  lmmbr2  24421  iscau3  24440  bcthlem5  24490  ovolunlem2  24660  dvres2  25074  dvfsumlem2  25189  plyadd  25376  plymul  25377  coeeu  25384  coemullem  25409  aalioulem4  25493  mulcxp  25838  cxplea  25849  cxple2  25850  cxplt2  25851  cxpcn3lem  25898  angcan  25950  ang180lem5  25961  divsqrtsumlem  26127  logexprlim  26371  dchrvmasumlema  26646  dchrisum0lema  26660  logdivsum  26679  log2sumbnd  26690  abvcxp  26761  padicabv  26776  tghilberti2  26997  brbtwn2  27271  axcontlem4  27333  axcontlem8  27337  clwlkl1loop  28147  clwwlknonex2lem2  28468  clwlknon2num  28728  numclwlk1lem2  28730  chscllem4  29998  orngmul  31498  measxun2  32174  measun  32175  mbfmco2  32228  probun  32382  satfv1fvfmla1  33381  nolesgn2ores  33871  nosupres  33906  nosupbnd1lem1  33907  nosupbnd1lem2  33908  nosupbnd1lem4  33910  nosupbnd1lem5  33911  nosupbnd1lem6  33912  noinffv  33920  noinfres  33921  noinfbnd1lem1  33922  noinfbnd1lem2  33923  noinfbnd1lem4  33925  noinfbnd1lem6  33927  nosupinfsep  33931  scutbdaylt  34008  cgrcomim  34287  cgrcoml  34294  cgrcomr  34295  cgrdegen  34302  btwnintr  34317  btwnexch3  34318  btwnouttr2  34320  btwnouttr  34322  btwnexch  34323  btwndiff  34325  lineid  34381  idinside  34382  btwnconn1lem7  34391  btwnconn1lem8  34392  btwnconn1lem9  34393  btwnconn1lem12  34396  btwnconn1lem14  34398  btwnconn3  34401  midofsegid  34402  segcon2  34403  brsegle2  34407  btwnoutside  34423  outsideoftr  34427  outsideofeu  34429  linethru  34451  cnres2  35917  heibor  35975  lsmsat  37018  lkrlsp  37112  lkrlsp2  37113  lkrlsp3  37114  latm4  37243  omlspjN  37271  hlatj4  37384  4noncolr3  37463  4noncolr2  37464  4noncolr1  37465  athgt  37466  3dimlem3a  37470  3dimlem4a  37473  3dimlem4  37474  3dimlem4OLDN  37475  3dim3  37479  1cvratex  37483  hlatexch4  37491  3atlem4  37496  atcvrlln2  37529  atcvrlln  37530  lplnnlelln  37553  lvoli2  37591  lvolnlelln  37594  lvolnlelpln  37595  4atlem11b  37618  4atlem12b  37621  2lplnja  37629  2lplnj  37630  dalemyeo  37642  dath2  37747  lncvrat  37792  cdlemblem  37803  cdlemb  37804  elpaddri  37812  padd4N  37850  llnmod2i2  37873  llnexchb2  37879  dalawlem1  37881  dalawlem2  37882  pclfinN  37910  osumcllem6N  37971  pexmidlem3N  37982  lhp2lt  38011  lhp2at0  38042  lhp2atnle  38043  lhp2atne  38044  lhp2at0nle  38045  lhp2at0ne  38046  lhpelim  38047  lhpmod2i2  38048  lhpmod6i1  38049  lhple  38052  lhpat  38053  lhpat3  38056  ltrncoelN  38153  ltrncoat  38154  ltrncnv  38156  trlat  38179  trl0  38180  ltrnnidn  38184  trlnid  38189  cdlemd7  38214  cdleme0b  38222  cdleme0c  38223  cdleme0fN  38228  cdleme02N  38232  cdleme0ex1N  38233  cdleme0ex2N  38234  cdleme7aa  38252  cdleme7c  38255  cdleme7d  38256  cdleme7e  38257  cdleme7ga  38258  cdleme7  38259  cdleme8  38260  cdleme11a  38270  cdleme17c  38298  cdleme22gb  38304  cdlemeda  38308  cdleme20k  38329  cdleme21a  38335  cdleme21d  38340  cdleme22f2  38357  cdleme22g  38358  cdleme23a  38359  cdleme23b  38360  cdleme23c  38361  cdleme24  38362  cdleme28  38383  cdlemefrs32fva1  38411  cdlemefr32sn2aw  38414  cdlemefs32sn1aw  38424  cdleme41sn3a  38443  cdleme32fva  38447  cdleme32fva1  38448  cdleme35a  38458  cdleme35b  38460  cdleme35c  38461  cdleme35f  38464  cdleme39a  38475  cdleme42a  38481  cdleme42c  38482  cdleme42b  38488  cdleme42e  38489  cdleme42f  38490  cdleme42g  38491  cdleme42h  38492  cdleme43bN  38500  cdleme46f2g2  38503  cdleme17d2  38505  cdleme17d4  38507  cdleme48fv  38509  cdleme48fvg  38510  cdleme4gfv  38517  cdlemeg46c  38523  cdlemeg46nlpq  38527  cdlemeg46gfre  38542  cdleme48d  38545  cdlemeg49lebilem  38549  cdleme50trn2  38561  cdleme50ltrn  38567  cdleme  38570  cdlemf1  38571  cdlemf  38573  trlord  38579  ltrniotacnvval  38592  ltrniotavalbN  38594  cdlemg1cex  38598  cdlemg2dN  38600  cdlemg2ce  38602  cdlemg2fvlem  38604  cdlemg2idN  38606  cdlemg2kq  38612  cdlemg2l  38613  cdlemg2m  38614  cdlemg4b2  38620  cdlemg7fvN  38634  cdlemg8a  38637  cdlemg10bALTN  38646  cdlemg11aq  38648  cdlemg12d  38656  cdlemg13a  38661  cdlemg13  38662  cdlemg14f  38663  cdlemg14g  38664  cdlemg17a  38671  cdlemg17b  38672  cdlemg27a  38702  cdlemg31b0N  38704  cdlemg31a  38707  cdlemg31b  38708  cdlemg31c  38709  ltrnco  38729  trlcoabs  38731  trlcoabs2N  38732  trlcocnvat  38734  trlconid  38735  trlcolem  38736  trlcone  38738  cdlemg42  38739  cdlemg43  38740  cdlemg46  38745  cdlemg47  38746  tendoeq1  38774  tendoco2  38778  tendoplco2  38789  tendopltp  38790  cdlemh1  38825  cdlemh2  38826  cdlemi1  38828  cdlemi  38830  cdlemk1  38841  cdlemk2  38842  cdlemk3  38843  cdlemk4  38844  cdlemk8  38848  cdlemk9  38849  cdlemk9bN  38850  cdlemk31  38906  cdlemk32  38907  cdlemk28-3  38918  cdlemk19u  38980  cdlemk56w  38983  tendoex  38985  erngdvlem4  39001  erngdvlem4-rN  39009  dia11N  39058  dib11N  39170  cdlemn6  39212  cdlemn7  39213  cdlemn8  39214  cdlemn9  39215  dihordlem6  39223  dihordlem7  39224  dihord1  39228  dihord2a  39229  dihord2b  39230  dihord2pre  39235  dihord2pre2  39236  dihlsscpre  39244  dihvalcq2  39257  dihopelvalcpre  39258  dihord4  39268  dihord6b  39270  dihmeetlem1N  39300  dihglblem3N  39305  dihmeetlem2N  39309  dihglbcpreN  39310  dihmeetcN  39312  dihmeetbclemN  39314  dihmeetlem4preN  39316  dihjatc1  39321  dihjatc2N  39322  dihjatc3  39323  dihmeetlem9N  39325  dihmeetlem13N  39329  dihmeetlem20N  39336  dih1dimatlem0  39338  mapdpglem24  39714  mapdpglem32  39715  baerlem3lem2  39720  baerlem5alem2  39721  baerlem5blem2  39722  mapdh9aOLDN  39800  hdmap14lem6  39883  nnadddir  40297  sn-addid2  40384  mzpsubst  40567  pellexlem5  40652  pellex  40654  pell14qrexpclnn0  40685  pellfundex  40705  qirropth  40727  monotuz  40760  congtr  40784  congmul  40786  congsub  40789  mzpcong  40791  fzmaxdif  40800  jm2.15nn0  40822  idomsubgmo  41020  iunrelexpmin1  41286  iunrelexpmin2  41290  trclimalb2  41304  mnringmulrcld  41816  fourierdlem42  43661  fourierdlem48  43666  fourierdlem80  43698  smfaddlem1  44266  prmdvdsfmtnof1lem1  45005  uspgropssxp  45275  lidldomn1  45448  rngccatidALTV  45516  coe1sclmulval  45695  lincdifsn  45734  seposep  46188  iscnrm3rlem8  46210  iscnrm3llem2  46213