Theorem simp2l 1195

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp12l  1282  simp22l  1288  simp32l  1294  fsnunf  6949  f1oiso2  7107  omeulem2  8211  uniinqs  8379  unxpdomlem3  8726  gruina  10242  dedekind  10805  addid2  10825  subaddmulsub  11105  dmdcan  11352  xaddass  12645  xaddass2  12646  xlt2add  12656  xmulasslem3  12682  xadddi2  12693  xadddi2r  12694  expaddzlem  13475  expaddz  13476  expmulz  13478  expdiv  13483  expmordi  13534  modexp  13602  pfxeq  14060  ccatopth2  14081  swrdco  14201  o1add  14972  o1mul  14973  o1sub  14974  fsumsplitsnun  15112  ntrivcvgmul  15260  prmexpb  16064  pcpremul  16182  pcdiv  16191  pcqmul  16192  pcqdiv  16196  4sqlem12  16294  f1ocpbllem  16799  ercpbl  16824  erlecpbl  16825  latjlej12  17679  latmlem12  17695  latj4  17713  latj4rot  17714  gsumsgrpccat  18006  gsmsymgreqlem2  18561  symgsssg  18597  symgfisg  18598  mndodcong  18672  cmn4  18928  ablsub4  18935  abladdsub4  18936  lsm4  18982  abvdom  19611  abvres  19612  abvtrivd  19613  lspsnvs  19888  lspsneu  19897  lspfixed  19902  lspexch  19903  lsmcv  19915  lspsolvlem  19916  coe1sclmulfv  20453  matvscacell  21047  m1detdiag  21208  cramerimplem3  21296  cnprest  21899  hausnei2  21963  isreg2  21987  cmpcld  22012  llyrest  22095  nllyrest  22096  elptr  22183  basqtop  22321  hausflimlem  22589  tmdgsum  22705  utop2nei  22861  trcfilu  22905  ssblps  23034  ssbl  23035  prdsxmslem2  23141  tgqioo  23410  metnrm  23472  bndth  23564  ncvspi  23762  ncvs1  23763  cph2ass  23819  lmmbr2  23864  iscau3  23883  bcthlem5  23933  ovolunlem2  24101  dvres2  24512  dvfsumlem2  24626  plyadd  24809  plymul  24810  coeeu  24817  coemullem  24842  aalioulem4  24926  mulcxp  25270  cxplea  25281  cxple2  25282  cxplt2  25283  cxpcn3lem  25330  angcan  25382  ang180lem5  25393  divsqrtsumlem  25559  logexprlim  25803  dchrvmasumlema  26078  dchrisum0lema  26092  logdivsum  26111  log2sumbnd  26122  abvcxp  26193  padicabv  26208  tghilberti2  26426  brbtwn2  26693  axcontlem4  26755  axcontlem8  26759  clwlkl1loop  27566  clwwlknonex2lem2  27889  clwlknon2num  28149  numclwlk1lem2  28151  chscllem4  29419  orngmul  30878  measxun2  31471  measun  31472  mbfmco2  31525  probun  31679  satfv1fvfmla1  32672  fpr3g  33124  nolesgn2ores  33181  nosupres  33209  nosupbnd1lem1  33210  nosupbnd1lem2  33211  nosupbnd1lem4  33213  nosupbnd1lem5  33214  nosupbnd1lem6  33215  scutbdaylt  33278  cgrcomim  33452  cgrcoml  33459  cgrcomr  33460  cgrdegen  33467  btwnintr  33482  btwnexch3  33483  btwnouttr2  33485  btwnouttr  33487  btwnexch  33488  btwndiff  33490  lineid  33546  idinside  33547  btwnconn1lem7  33556  btwnconn1lem8  33557  btwnconn1lem9  33558  btwnconn1lem12  33561  btwnconn1lem14  33563  btwnconn3  33566  midofsegid  33567  segcon2  33568  brsegle2  33572  btwnoutside  33588  outsideoftr  33592  outsideofeu  33594  linethru  33616  cnres2  35043  heibor  35101  lsmsat  36146  lkrlsp  36240  lkrlsp2  36241  lkrlsp3  36242  latm4  36371  omlspjN  36399  hlatj4  36512  4noncolr3  36591  4noncolr2  36592  4noncolr1  36593  athgt  36594  3dimlem3a  36598  3dimlem4a  36601  3dimlem4  36602  3dimlem4OLDN  36603  3dim3  36607  1cvratex  36611  hlatexch4  36619  3atlem4  36624  atcvrlln2  36657  atcvrlln  36658  lplnnlelln  36681  lvoli2  36719  lvolnlelln  36722  lvolnlelpln  36723  4atlem11b  36746  4atlem12b  36749  2lplnja  36757  2lplnj  36758  dalemyeo  36770  dath2  36875  lncvrat  36920  cdlemblem  36931  cdlemb  36932  elpaddri  36940  padd4N  36978  llnmod2i2  37001  llnexchb2  37007  dalawlem1  37009  dalawlem2  37010  pclfinN  37038  osumcllem6N  37099  pexmidlem3N  37110  lhp2lt  37139  lhp2at0  37170  lhp2atnle  37171  lhp2atne  37172  lhp2at0nle  37173  lhp2at0ne  37174  lhpelim  37175  lhpmod2i2  37176  lhpmod6i1  37177  lhple  37180  lhpat  37181  lhpat3  37184  ltrncoelN  37281  ltrncoat  37282  ltrncnv  37284  trlat  37307  trl0  37308  ltrnnidn  37312  trlnid  37317  cdlemd7  37342  cdleme0b  37350  cdleme0c  37351  cdleme0fN  37356  cdleme02N  37360  cdleme0ex1N  37361  cdleme0ex2N  37362  cdleme7aa  37380  cdleme7c  37383  cdleme7d  37384  cdleme7e  37385  cdleme7ga  37386  cdleme7  37387  cdleme8  37388  cdleme11a  37398  cdleme17c  37426  cdleme22gb  37432  cdlemeda  37436  cdleme20k  37457  cdleme21a  37463  cdleme21d  37468  cdleme22f2  37485  cdleme22g  37486  cdleme23a  37487  cdleme23b  37488  cdleme23c  37489  cdleme24  37490  cdleme28  37511  cdlemefrs32fva1  37539  cdlemefr32sn2aw  37542  cdlemefs32sn1aw  37552  cdleme41sn3a  37571  cdleme32fva  37575  cdleme32fva1  37576  cdleme35a  37586  cdleme35b  37588  cdleme35c  37589  cdleme35f  37592  cdleme39a  37603  cdleme42a  37609  cdleme42c  37610  cdleme42b  37616  cdleme42e  37617  cdleme42f  37618  cdleme42g  37619  cdleme42h  37620  cdleme43bN  37628  cdleme46f2g2  37631  cdleme17d2  37633  cdleme17d4  37635  cdleme48fv  37637  cdleme48fvg  37638  cdleme4gfv  37645  cdlemeg46c  37651  cdlemeg46nlpq  37655  cdlemeg46gfre  37670  cdleme48d  37673  cdlemeg49lebilem  37677  cdleme50trn2  37689  cdleme50ltrn  37695  cdleme  37698  cdlemf1  37699  cdlemf  37701  trlord  37707  ltrniotacnvval  37720  ltrniotavalbN  37722  cdlemg1cex  37726  cdlemg2dN  37728  cdlemg2ce  37730  cdlemg2fvlem  37732  cdlemg2idN  37734  cdlemg2kq  37740  cdlemg2l  37741  cdlemg2m  37742  cdlemg4b2  37748  cdlemg7fvN  37762  cdlemg8a  37765  cdlemg10bALTN  37774  cdlemg11aq  37776  cdlemg12d  37784  cdlemg13a  37789  cdlemg13  37790  cdlemg14f  37791  cdlemg14g  37792  cdlemg17a  37799  cdlemg17b  37800  cdlemg27a  37830  cdlemg31b0N  37832  cdlemg31a  37835  cdlemg31b  37836  cdlemg31c  37837  ltrnco  37857  trlcoabs  37859  trlcoabs2N  37860  trlcocnvat  37862  trlconid  37863  trlcolem  37864  trlcone  37866  cdlemg42  37867  cdlemg43  37868  cdlemg46  37873  cdlemg47  37874  tendoeq1  37902  tendoco2  37906  tendoplco2  37917  tendopltp  37918  cdlemh1  37953  cdlemh2  37954  cdlemi1  37956  cdlemi  37958  cdlemk1  37969  cdlemk2  37970  cdlemk3  37971  cdlemk4  37972  cdlemk8  37976  cdlemk9  37977  cdlemk9bN  37978  cdlemk31  38034  cdlemk32  38035  cdlemk28-3  38046  cdlemk19u  38108  cdlemk56w  38111  tendoex  38113  erngdvlem4  38129  erngdvlem4-rN  38137  dia11N  38186  dib11N  38298  cdlemn6  38340  cdlemn7  38341  cdlemn8  38342  cdlemn9  38343  dihordlem6  38351  dihordlem7  38352  dihord1  38356  dihord2a  38357  dihord2b  38358  dihord2pre  38363  dihord2pre2  38364  dihlsscpre  38372  dihvalcq2  38385  dihopelvalcpre  38386  dihord4  38396  dihord6b  38398  dihmeetlem1N  38428  dihglblem3N  38433  dihmeetlem2N  38437  dihglbcpreN  38438  dihmeetcN  38440  dihmeetbclemN  38442  dihmeetlem4preN  38444  dihjatc1  38449  dihjatc2N  38450  dihjatc3  38451  dihmeetlem9N  38453  dihmeetlem13N  38457  dihmeetlem20N  38464  dih1dimatlem0  38466  mapdpglem24  38842  mapdpglem32  38843  baerlem3lem2  38848  baerlem5alem2  38849  baerlem5blem2  38850  mapdh9aOLDN  38928  hdmap14lem6  39011  nnadddir  39170  sn-addid2  39241  mzpsubst  39352  pellexlem5  39437  pellex  39439  pell14qrexpclnn0  39470  pellfundex  39490  qirropth  39512  monotuz  39545  congtr  39569  congmul  39571  congsub  39574  mzpcong  39576  fzmaxdif  39585  jm2.15nn0  39607  idomsubgmo  39805  iunrelexpmin1  40060  iunrelexpmin2  40064  trclimalb2  40078  fourierdlem42  42441  fourierdlem48  42446  fourierdlem80  42478  smfaddlem1  43046  prmdvdsfmtnof1lem1  43753  uspgropssxp  44026  lidldomn1  44199  rngccatidALTV  44267  coe1sclmulval  44446  lincdifsn  44486