Theorem simp2l 1206

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 1140	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp12l  1293  simp22l  1299  simp32l  1305  fsnunf  7136  f1oiso2  7303  fpr3g  8232  omeulem2  8515  uniinqs  8741  unxpdomlem3  9165  gruina  10739  dedekind  11307  addlid  11327  subaddmulsub  11611  dmdcan  11863  nnadddir  12231  xaddass  13199  xaddass2  13200  xlt2add  13210  xmulasslem3  13236  xadddi2  13247  xadddi2r  13248  expaddzlem  14065  expaddz  14066  expmulz  14068  expdiv  14073  expmordi  14127  modexp  14198  pfxeq  14656  ccatopth2  14677  swrdco  14797  o1add  15574  o1mul  15575  o1sub  15576  fsumsplitsnun  15715  ntrivcvgmul  15865  prmexpb  16687  pcpremul  16812  pcdiv  16821  pcqmul  16822  pcqdiv  16826  4sqlem12  16925  f1ocpbllem  17486  ercpbl  17511  erlecpbl  17512  latjlej12  18419  latmlem12  18435  latj4  18453  latj4rot  18454  gsumsgrpccat  18806  gsmsymgreqlem2  19404  symgsssg  19440  symgfisg  19441  mndodcong  19515  cmn4  19774  ablsub4  19783  abladdsub4  19784  lsm4  19833  abvdom  20809  abvres  20810  abvtrivd  20811  orngmul  20844  lspsnvs  21114  lspsneu  21123  lspfixed  21128  lspexch  21129  lsmcv  21141  lspsolvlem  21142  ring2idlqus1  21319  coe1sclmulfv  22276  matvscacell  22426  m1detdiag  22587  cramerimplem3  22675  cnprest  23279  hausnei2  23343  isreg2  23367  cmpcld  23392  llyrest  23475  nllyrest  23476  elptr  23563  basqtop  23701  hausflimlem  23969  tmdgsum  24085  utop2nei  24240  trcfilu  24283  ssblps  24412  ssbl  24413  prdsxmslem2  24519  tgqioo  24790  metnrm  24853  bndth  24950  ncvspi  25148  ncvs1  25149  cph2ass  25205  lmmbr2  25251  iscau3  25270  bcthlem5  25320  ovolunlem2  25490  dvres2  25904  dvfsumlem2  26019  plyadd  26207  plymul  26208  coeeu  26215  coemullem  26240  aalioulem4  26326  mulcxp  26674  cxplea  26685  cxple2  26686  cxplt2  26687  cxpcn3lem  26736  angcan  26791  ang180lem5  26802  divsqrtsumlem  26968  logexprlim  27213  dchrvmasumlema  27488  dchrisum0lema  27502  logdivsum  27521  log2sumbnd  27532  abvcxp  27603  padicabv  27618  nolesgn2ores  27661  nosupres  27696  nosupbnd1lem1  27697  nosupbnd1lem2  27698  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd1lem6  27702  noinffv  27710  noinfres  27711  noinfbnd1lem1  27712  noinfbnd1lem2  27713  noinfbnd1lem4  27715  noinfbnd1lem6  27717  nosupinfsep  27721  cutbdaylt  27815  expsgt0  28454  bdayfinbndlem1  28484  tghilberti2  28731  brbtwn2  28999  axcontlem4  29061  axcontlem8  29065  clwlkl1loop  29876  clwwlknonex2lem2  30203  clwlknon2num  30463  numclwlk1lem2  30465  chscllem4  31736  measxun2  34401  measun  34402  mbfmco2  34456  probun  34610  satfv1fvfmla1  35658  cgrcomim  36224  cgrcoml  36231  cgrcomr  36232  cgrdegen  36239  btwnintr  36254  btwnexch3  36255  btwnouttr2  36257  btwnouttr  36259  btwnexch  36260  btwndiff  36262  lineid  36318  idinside  36319  btwnconn1lem7  36328  btwnconn1lem8  36329  btwnconn1lem9  36330  btwnconn1lem12  36333  btwnconn1lem14  36335  btwnconn3  36338  midofsegid  36339  segcon2  36340  brsegle2  36344  btwnoutside  36360  outsideoftr  36364  outsideofeu  36366  linethru  36388  cnres2  38137  heibor  38195  lsmsat  39507  lkrlsp  39601  lkrlsp2  39602  lkrlsp3  39603  latm4  39732  omlspjN  39760  hlatj4  39873  4noncolr3  39952  4noncolr2  39953  4noncolr1  39954  athgt  39955  3dimlem3a  39959  3dimlem4a  39962  3dimlem4  39963  3dimlem4OLDN  39964  3dim3  39968  1cvratex  39972  hlatexch4  39980  3atlem4  39985  atcvrlln2  40018  atcvrlln  40019  lplnnlelln  40042  lvoli2  40080  lvolnlelln  40083  lvolnlelpln  40084  4atlem11b  40107  4atlem12b  40110  2lplnja  40118  2lplnj  40119  dalemyeo  40131  dath2  40236  lncvrat  40281  cdlemblem  40292  cdlemb  40293  elpaddri  40301  padd4N  40339  llnmod2i2  40362  llnexchb2  40368  dalawlem1  40370  dalawlem2  40371  pclfinN  40399  osumcllem6N  40460  pexmidlem3N  40471  lhp2lt  40500  lhp2at0  40531  lhp2atnle  40532  lhp2atne  40533  lhp2at0nle  40534  lhp2at0ne  40535  lhpelim  40536  lhpmod2i2  40537  lhpmod6i1  40538  lhple  40541  lhpat  40542  lhpat3  40545  ltrncoelN  40642  ltrncoat  40643  ltrncnv  40645  trlat  40668  trl0  40669  ltrnnidn  40673  trlnid  40678  cdlemd7  40703  cdleme0b  40711  cdleme0c  40712  cdleme0fN  40717  cdleme02N  40721  cdleme0ex1N  40722  cdleme0ex2N  40723  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme8  40749  cdleme11a  40759  cdleme17c  40787  cdleme22gb  40793  cdlemeda  40797  cdleme20k  40818  cdleme21a  40824  cdleme21d  40829  cdleme22f2  40846  cdleme22g  40847  cdleme23a  40848  cdleme23b  40849  cdleme23c  40850  cdleme24  40851  cdleme28  40872  cdlemefrs32fva1  40900  cdlemefr32sn2aw  40903  cdlemefs32sn1aw  40913  cdleme41sn3a  40932  cdleme32fva  40936  cdleme32fva1  40937  cdleme35a  40947  cdleme35b  40949  cdleme35c  40950  cdleme35f  40953  cdleme39a  40964  cdleme42a  40970  cdleme42c  40971  cdleme42b  40977  cdleme42e  40978  cdleme42f  40979  cdleme42g  40980  cdleme42h  40981  cdleme43bN  40989  cdleme46f2g2  40992  cdleme17d2  40994  cdleme17d4  40996  cdleme48fv  40998  cdleme48fvg  40999  cdleme4gfv  41006  cdlemeg46c  41012  cdlemeg46nlpq  41016  cdlemeg46gfre  41031  cdleme48d  41034  cdlemeg49lebilem  41038  cdleme50trn2  41050  cdleme50ltrn  41056  cdleme  41059  cdlemf1  41060  cdlemf  41062  trlord  41068  ltrniotacnvval  41081  ltrniotavalbN  41083  cdlemg1cex  41087  cdlemg2dN  41089  cdlemg2ce  41091  cdlemg2fvlem  41093  cdlemg2idN  41095  cdlemg2kq  41101  cdlemg2l  41102  cdlemg2m  41103  cdlemg4b2  41109  cdlemg7fvN  41123  cdlemg8a  41126  cdlemg10bALTN  41135  cdlemg11aq  41137  cdlemg12d  41145  cdlemg13a  41150  cdlemg13  41151  cdlemg14f  41152  cdlemg14g  41153  cdlemg17a  41160  cdlemg17b  41161  cdlemg27a  41191  cdlemg31b0N  41193  cdlemg31a  41196  cdlemg31b  41197  cdlemg31c  41198  ltrnco  41218  trlcoabs  41220  trlcoabs2N  41221  trlcocnvat  41223  trlconid  41224  trlcolem  41225  trlcone  41227  cdlemg42  41228  cdlemg43  41229  cdlemg46  41234  cdlemg47  41235  tendoeq1  41263  tendoco2  41267  tendoplco2  41278  tendopltp  41279  cdlemh1  41314  cdlemh2  41315  cdlemi1  41317  cdlemi  41319  cdlemk1  41330  cdlemk2  41331  cdlemk3  41332  cdlemk4  41333  cdlemk8  41337  cdlemk9  41338  cdlemk9bN  41339  cdlemk31  41395  cdlemk32  41396  cdlemk28-3  41407  cdlemk19u  41469  cdlemk56w  41472  tendoex  41474  erngdvlem4  41490  erngdvlem4-rN  41498  dia11N  41547  dib11N  41659  cdlemn6  41701  cdlemn7  41702  cdlemn8  41703  cdlemn9  41704  dihordlem6  41712  dihordlem7  41713  dihord1  41717  dihord2a  41718  dihord2b  41719  dihord2pre  41724  dihord2pre2  41725  dihlsscpre  41733  dihvalcq2  41746  dihopelvalcpre  41747  dihord4  41757  dihord6b  41759  dihmeetlem1N  41789  dihglblem3N  41794  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetcN  41801  dihmeetbclemN  41803  dihmeetlem4preN  41805  dihjatc1  41810  dihjatc2N  41811  dihjatc3  41812  dihmeetlem9N  41814  dihmeetlem13N  41818  dihmeetlem20N  41825  dih1dimatlem0  41827  mapdpglem24  42203  mapdpglem32  42204  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  mapdh9aOLDN  42289  hdmap14lem6  42372  sn-addlid  42888  mzpsubst  43204  pellexlem5  43285  pellex  43287  pell14qrexpclnn0  43318  pellfundex  43338  qirropth  43360  monotuz  43393  congtr  43417  congmul  43419  congsub  43422  mzpcong  43424  fzmaxdif  43433  jm2.15nn0  43455  idomsubgmo  43645  iunrelexpmin1  44159  iunrelexpmin2  44163  trclimalb2  44177  mnringmulrcld  44679  fourierdlem42  46599  fourierdlem48  46604  fourierdlem80  46636  smfaddlem1  47213  prmdvdsfmtnof1lem1  48069  uhgrimisgrgric  48429  uspgropssxp  48642  lidldomn1  48729  rngccatidALTV  48770  coe1sclmulval  48883  lincdifsn  48922  seposep  49423  iscnrm3rlem8  49444  iscnrm3llem2  49447