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  7176  f1oiso2  7344  fpr3g  8282  omeulem2  8593  uniinqs  8809  unxpdomlem3  9258  gruina  10830  dedekind  11396  addlid  11416  subaddmulsub  11698  dmdcan  11949  xaddass  13263  xaddass2  13264  xlt2add  13274  xmulasslem3  13300  xadddi2  13311  xadddi2r  13312  expaddzlem  14121  expaddz  14122  expmulz  14124  expdiv  14129  expmordi  14183  modexp  14254  pfxeq  14712  ccatopth2  14733  swrdco  14854  o1add  15628  o1mul  15629  o1sub  15630  fsumsplitsnun  15769  ntrivcvgmul  15916  prmexpb  16736  pcpremul  16861  pcdiv  16870  pcqmul  16871  pcqdiv  16875  4sqlem12  16974  f1ocpbllem  17536  ercpbl  17561  erlecpbl  17562  latjlej12  18463  latmlem12  18479  latj4  18497  latj4rot  18498  gsumsgrpccat  18816  gsmsymgreqlem2  19410  symgsssg  19446  symgfisg  19447  mndodcong  19521  cmn4  19780  ablsub4  19789  abladdsub4  19790  lsm4  19839  abvdom  20788  abvres  20789  abvtrivd  20790  lspsnvs  21073  lspsneu  21082  lspfixed  21087  lspexch  21088  lsmcv  21100  lspsolvlem  21101  ring2idlqus1  21278  coe1sclmulfv  22218  matvscacell  22372  m1detdiag  22533  cramerimplem3  22621  cnprest  23225  hausnei2  23289  isreg2  23313  cmpcld  23338  llyrest  23421  nllyrest  23422  elptr  23509  basqtop  23647  hausflimlem  23915  tmdgsum  24031  utop2nei  24187  trcfilu  24230  ssblps  24359  ssbl  24360  prdsxmslem2  24466  tgqioo  24737  metnrm  24800  bndth  24906  ncvspi  25106  ncvs1  25107  cph2ass  25163  lmmbr2  25209  iscau3  25228  bcthlem5  25278  ovolunlem2  25449  dvres2  25863  dvfsumlem2  25983  dvfsumlem2OLD  25984  plyadd  26172  plymul  26173  coeeu  26180  coemullem  26205  aalioulem4  26293  mulcxp  26644  cxplea  26655  cxple2  26656  cxplt2  26657  cxpcn3lem  26707  angcan  26762  ang180lem5  26773  divsqrtsumlem  26940  logexprlim  27186  dchrvmasumlema  27461  dchrisum0lema  27475  logdivsum  27494  log2sumbnd  27505  abvcxp  27576  padicabv  27591  nolesgn2ores  27634  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem2  27671  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd1lem6  27675  noinffv  27683  noinfres  27684  noinfbnd1lem1  27685  noinfbnd1lem2  27686  noinfbnd1lem4  27688  noinfbnd1lem6  27690  nosupinfsep  27694  scutbdaylt  27780  expsgt0  28332  tghilberti2  28563  brbtwn2  28830  axcontlem4  28892  axcontlem8  28896  clwlkl1loop  29711  clwwlknonex2lem2  30035  clwlknon2num  30295  numclwlk1lem2  30297  chscllem4  31567  orngmul  33271  measxun2  34187  measun  34188  mbfmco2  34243  probun  34397  satfv1fvfmla1  35391  cgrcomim  35953  cgrcoml  35960  cgrcomr  35961  cgrdegen  35968  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  btwnouttr  35988  btwnexch  35989  btwndiff  35991  lineid  36047  idinside  36048  btwnconn1lem7  36057  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem12  36062  btwnconn1lem14  36064  btwnconn3  36067  midofsegid  36068  segcon2  36069  brsegle2  36073  btwnoutside  36089  outsideoftr  36093  outsideofeu  36095  linethru  36117  cnres2  37733  heibor  37791  lsmsat  38972  lkrlsp  39066  lkrlsp2  39067  lkrlsp3  39068  latm4  39197  omlspjN  39225  hlatj4  39338  4noncolr3  39418  4noncolr2  39419  4noncolr1  39420  athgt  39421  3dimlem3a  39425  3dimlem4a  39428  3dimlem4  39429  3dimlem4OLDN  39430  3dim3  39434  1cvratex  39438  hlatexch4  39446  3atlem4  39451  atcvrlln2  39484  atcvrlln  39485  lplnnlelln  39508  lvoli2  39546  lvolnlelln  39549  lvolnlelpln  39550  4atlem11b  39573  4atlem12b  39576  2lplnja  39584  2lplnj  39585  dalemyeo  39597  dath2  39702  lncvrat  39747  cdlemblem  39758  cdlemb  39759  elpaddri  39767  padd4N  39805  llnmod2i2  39828  llnexchb2  39834  dalawlem1  39836  dalawlem2  39837  pclfinN  39865  osumcllem6N  39926  pexmidlem3N  39937  lhp2lt  39966  lhp2at0  39997  lhp2atnle  39998  lhp2atne  39999  lhp2at0nle  40000  lhp2at0ne  40001  lhpelim  40002  lhpmod2i2  40003  lhpmod6i1  40004  lhple  40007  lhpat  40008  lhpat3  40011  ltrncoelN  40108  ltrncoat  40109  ltrncnv  40111  trlat  40134  trl0  40135  ltrnnidn  40139  trlnid  40144  cdlemd7  40169  cdleme0b  40177  cdleme0c  40178  cdleme0fN  40183  cdleme02N  40187  cdleme0ex1N  40188  cdleme0ex2N  40189  cdleme7aa  40207  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme8  40215  cdleme11a  40225  cdleme17c  40253  cdleme22gb  40259  cdlemeda  40263  cdleme20k  40284  cdleme21a  40290  cdleme21d  40295  cdleme22f2  40312  cdleme22g  40313  cdleme23a  40314  cdleme23b  40315  cdleme23c  40316  cdleme24  40317  cdleme28  40338  cdlemefrs32fva1  40366  cdlemefr32sn2aw  40369  cdlemefs32sn1aw  40379  cdleme41sn3a  40398  cdleme32fva  40402  cdleme32fva1  40403  cdleme35a  40413  cdleme35b  40415  cdleme35c  40416  cdleme35f  40419  cdleme39a  40430  cdleme42a  40436  cdleme42c  40437  cdleme42b  40443  cdleme42e  40444  cdleme42f  40445  cdleme42g  40446  cdleme42h  40447  cdleme43bN  40455  cdleme46f2g2  40458  cdleme17d2  40460  cdleme17d4  40462  cdleme48fv  40464  cdleme48fvg  40465  cdleme4gfv  40472  cdlemeg46c  40478  cdlemeg46nlpq  40482  cdlemeg46gfre  40497  cdleme48d  40500  cdlemeg49lebilem  40504  cdleme50trn2  40516  cdleme50ltrn  40522  cdleme  40525  cdlemf1  40526  cdlemf  40528  trlord  40534  ltrniotacnvval  40547  ltrniotavalbN  40549  cdlemg1cex  40553  cdlemg2dN  40555  cdlemg2ce  40557  cdlemg2fvlem  40559  cdlemg2idN  40561  cdlemg2kq  40567  cdlemg2l  40568  cdlemg2m  40569  cdlemg4b2  40575  cdlemg7fvN  40589  cdlemg8a  40592  cdlemg10bALTN  40601  cdlemg11aq  40603  cdlemg12d  40611  cdlemg13a  40616  cdlemg13  40617  cdlemg14f  40618  cdlemg14g  40619  cdlemg17a  40626  cdlemg17b  40627  cdlemg27a  40657  cdlemg31b0N  40659  cdlemg31a  40662  cdlemg31b  40663  cdlemg31c  40664  ltrnco  40684  trlcoabs  40686  trlcoabs2N  40687  trlcocnvat  40689  trlconid  40690  trlcolem  40691  trlcone  40693  cdlemg42  40694  cdlemg43  40695  cdlemg46  40700  cdlemg47  40701  tendoeq1  40729  tendoco2  40733  tendoplco2  40744  tendopltp  40745  cdlemh1  40780  cdlemh2  40781  cdlemi1  40783  cdlemi  40785  cdlemk1  40796  cdlemk2  40797  cdlemk3  40798  cdlemk4  40799  cdlemk8  40803  cdlemk9  40804  cdlemk9bN  40805  cdlemk31  40861  cdlemk32  40862  cdlemk28-3  40873  cdlemk19u  40935  cdlemk56w  40938  tendoex  40940  erngdvlem4  40956  erngdvlem4-rN  40964  dia11N  41013  dib11N  41125  cdlemn6  41167  cdlemn7  41168  cdlemn8  41169  cdlemn9  41170  dihordlem6  41178  dihordlem7  41179  dihord1  41183  dihord2a  41184  dihord2b  41185  dihord2pre  41190  dihord2pre2  41191  dihlsscpre  41199  dihvalcq2  41212  dihopelvalcpre  41213  dihord4  41223  dihord6b  41225  dihmeetlem1N  41255  dihglblem3N  41260  dihmeetlem2N  41264  dihglbcpreN  41265  dihmeetcN  41267  dihmeetbclemN  41269  dihmeetlem4preN  41271  dihjatc1  41276  dihjatc2N  41277  dihjatc3  41278  dihmeetlem9N  41280  dihmeetlem13N  41284  dihmeetlem20N  41291  dih1dimatlem0  41293  mapdpglem24  41669  mapdpglem32  41670  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  mapdh9aOLDN  41755  hdmap14lem6  41838  nnadddir  42267  sn-addlid  42394  mzpsubst  42718  pellexlem5  42803  pellex  42805  pell14qrexpclnn0  42836  pellfundex  42856  qirropth  42878  monotuz  42912  congtr  42936  congmul  42938  congsub  42941  mzpcong  42943  fzmaxdif  42952  jm2.15nn0  42974  idomsubgmo  43164  iunrelexpmin1  43679  iunrelexpmin2  43683  trclimalb2  43697  mnringmulrcld  44200  fourierdlem42  46126  fourierdlem48  46131  fourierdlem80  46163  smfaddlem1  46740  prmdvdsfmtnof1lem1  47546  uhgrimisgrgric  47892  uspgropssxp  48067  lidldomn1  48154  rngccatidALTV  48195  coe1sclmulval  48309  lincdifsn  48348  seposep  48848  iscnrm3rlem8  48869  iscnrm3llem2  48872