Theorem simp2l 1201

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  1288  simp22l  1294  simp32l  1300  fsnunf  7140  f1oiso2  7307  fpr3g  8235  omeulem2  8518  uniinqs  8744  unxpdomlem3  9168  gruina  10741  dedekind  11309  addlid  11329  subaddmulsub  11613  dmdcan  11865  nnadddir  12233  xaddass  13201  xaddass2  13202  xlt2add  13212  xmulasslem3  13238  xadddi2  13249  xadddi2r  13250  expaddzlem  14067  expaddz  14068  expmulz  14070  expdiv  14075  expmordi  14129  modexp  14200  pfxeq  14658  ccatopth2  14679  swrdco  14799  o1add  15576  o1mul  15577  o1sub  15578  fsumsplitsnun  15717  ntrivcvgmul  15867  prmexpb  16689  pcpremul  16814  pcdiv  16823  pcqmul  16824  pcqdiv  16828  4sqlem12  16927  f1ocpbllem  17488  ercpbl  17513  erlecpbl  17514  latjlej12  18421  latmlem12  18437  latj4  18455  latj4rot  18456  gsumsgrpccat  18808  gsmsymgreqlem2  19406  symgsssg  19442  symgfisg  19443  mndodcong  19517  cmn4  19776  ablsub4  19785  abladdsub4  19786  lsm4  19835  abvdom  20807  abvres  20808  abvtrivd  20809  orngmul  20842  lspsnvs  21112  lspsneu  21121  lspfixed  21126  lspexch  21127  lsmcv  21139  lspsolvlem  21140  ring2idlqus1  21317  coe1sclmulfv  22248  matvscacell  22401  m1detdiag  22562  cramerimplem3  22650  cnprest  23254  hausnei2  23318  isreg2  23342  cmpcld  23367  llyrest  23450  nllyrest  23451  elptr  23538  basqtop  23676  hausflimlem  23944  tmdgsum  24060  utop2nei  24215  trcfilu  24258  ssblps  24387  ssbl  24388  prdsxmslem2  24494  tgqioo  24765  metnrm  24828  bndth  24925  ncvspi  25123  ncvs1  25124  cph2ass  25180  lmmbr2  25226  iscau3  25245  bcthlem5  25295  ovolunlem2  25465  dvres2  25879  dvfsumlem2  25994  plyadd  26182  plymul  26183  coeeu  26190  coemullem  26215  aalioulem4  26301  mulcxp  26649  cxplea  26660  cxple2  26661  cxplt2  26662  cxpcn3lem  26711  angcan  26766  ang180lem5  26777  divsqrtsumlem  26943  logexprlim  27188  dchrvmasumlema  27463  dchrisum0lema  27477  logdivsum  27496  log2sumbnd  27507  abvcxp  27578  padicabv  27593  nolesgn2ores  27636  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem2  27673  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd1lem6  27677  noinffv  27685  noinfres  27686  noinfbnd1lem1  27687  noinfbnd1lem2  27688  noinfbnd1lem4  27690  noinfbnd1lem6  27692  nosupinfsep  27696  cutbdaylt  27790  expsgt0  28429  bdayfinbndlem1  28459  tghilberti2  28706  brbtwn2  28974  axcontlem4  29036  axcontlem8  29040  clwlkl1loop  29851  clwwlknonex2lem2  30178  clwlknon2num  30438  numclwlk1lem2  30440  chscllem4  31711  measxun2  34354  measun  34355  mbfmco2  34409  probun  34563  satfv1fvfmla1  35605  cgrcomim  36171  cgrcoml  36178  cgrcomr  36179  cgrdegen  36186  btwnintr  36201  btwnexch3  36202  btwnouttr2  36204  btwnouttr  36206  btwnexch  36207  btwndiff  36209  lineid  36265  idinside  36266  btwnconn1lem7  36275  btwnconn1lem8  36276  btwnconn1lem9  36277  btwnconn1lem12  36280  btwnconn1lem14  36282  btwnconn3  36285  midofsegid  36286  segcon2  36287  brsegle2  36291  btwnoutside  36307  outsideoftr  36311  outsideofeu  36313  linethru  36335  cnres2  38084  heibor  38142  lsmsat  39454  lkrlsp  39548  lkrlsp2  39549  lkrlsp3  39550  latm4  39679  omlspjN  39707  hlatj4  39820  4noncolr3  39899  4noncolr2  39900  4noncolr1  39901  athgt  39902  3dimlem3a  39906  3dimlem4a  39909  3dimlem4  39910  3dimlem4OLDN  39911  3dim3  39915  1cvratex  39919  hlatexch4  39927  3atlem4  39932  atcvrlln2  39965  atcvrlln  39966  lplnnlelln  39989  lvoli2  40027  lvolnlelln  40030  lvolnlelpln  40031  4atlem11b  40054  4atlem12b  40057  2lplnja  40065  2lplnj  40066  dalemyeo  40078  dath2  40183  lncvrat  40228  cdlemblem  40239  cdlemb  40240  elpaddri  40248  padd4N  40286  llnmod2i2  40309  llnexchb2  40315  dalawlem1  40317  dalawlem2  40318  pclfinN  40346  osumcllem6N  40407  pexmidlem3N  40418  lhp2lt  40447  lhp2at0  40478  lhp2atnle  40479  lhp2atne  40480  lhp2at0nle  40481  lhp2at0ne  40482  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  lhple  40488  lhpat  40489  lhpat3  40492  ltrncoelN  40589  ltrncoat  40590  ltrncnv  40592  trlat  40615  trl0  40616  ltrnnidn  40620  trlnid  40625  cdlemd7  40650  cdleme0b  40658  cdleme0c  40659  cdleme0fN  40664  cdleme02N  40668  cdleme0ex1N  40669  cdleme0ex2N  40670  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme8  40696  cdleme11a  40706  cdleme17c  40734  cdleme22gb  40740  cdlemeda  40744  cdleme20k  40765  cdleme21a  40771  cdleme21d  40776  cdleme22f2  40793  cdleme22g  40794  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme24  40798  cdleme28  40819  cdlemefrs32fva1  40847  cdlemefr32sn2aw  40850  cdlemefs32sn1aw  40860  cdleme41sn3a  40879  cdleme32fva  40883  cdleme32fva1  40884  cdleme35a  40894  cdleme35b  40896  cdleme35c  40897  cdleme35f  40900  cdleme39a  40911  cdleme42a  40917  cdleme42c  40918  cdleme42b  40924  cdleme42e  40925  cdleme42f  40926  cdleme42g  40927  cdleme42h  40928  cdleme43bN  40936  cdleme46f2g2  40939  cdleme17d2  40941  cdleme17d4  40943  cdleme48fv  40945  cdleme48fvg  40946  cdleme4gfv  40953  cdlemeg46c  40959  cdlemeg46nlpq  40963  cdlemeg46gfre  40978  cdleme48d  40981  cdlemeg49lebilem  40985  cdleme50trn2  40997  cdleme50ltrn  41003  cdleme  41006  cdlemf1  41007  cdlemf  41009  trlord  41015  ltrniotacnvval  41028  ltrniotavalbN  41030  cdlemg1cex  41034  cdlemg2dN  41036  cdlemg2ce  41038  cdlemg2fvlem  41040  cdlemg2idN  41042  cdlemg2kq  41048  cdlemg2l  41049  cdlemg2m  41050  cdlemg4b2  41056  cdlemg7fvN  41070  cdlemg8a  41073  cdlemg10bALTN  41082  cdlemg11aq  41084  cdlemg12d  41092  cdlemg13a  41097  cdlemg13  41098  cdlemg14f  41099  cdlemg14g  41100  cdlemg17a  41107  cdlemg17b  41108  cdlemg27a  41138  cdlemg31b0N  41140  cdlemg31a  41143  cdlemg31b  41144  cdlemg31c  41145  ltrnco  41165  trlcoabs  41167  trlcoabs2N  41168  trlcocnvat  41170  trlconid  41171  trlcolem  41172  trlcone  41174  cdlemg42  41175  cdlemg43  41176  cdlemg46  41181  cdlemg47  41182  tendoeq1  41210  tendoco2  41214  tendoplco2  41225  tendopltp  41226  cdlemh1  41261  cdlemh2  41262  cdlemi1  41264  cdlemi  41266  cdlemk1  41277  cdlemk2  41278  cdlemk3  41279  cdlemk4  41280  cdlemk8  41284  cdlemk9  41285  cdlemk9bN  41286  cdlemk31  41342  cdlemk32  41343  cdlemk28-3  41354  cdlemk19u  41416  cdlemk56w  41419  tendoex  41421  erngdvlem4  41437  erngdvlem4-rN  41445  dia11N  41494  dib11N  41606  cdlemn6  41648  cdlemn7  41649  cdlemn8  41650  cdlemn9  41651  dihordlem6  41659  dihordlem7  41660  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord2pre  41671  dihord2pre2  41672  dihlsscpre  41680  dihvalcq2  41693  dihopelvalcpre  41694  dihord4  41704  dihord6b  41706  dihmeetlem1N  41736  dihglblem3N  41741  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetcN  41748  dihmeetbclemN  41750  dihmeetlem4preN  41752  dihjatc1  41757  dihjatc2N  41758  dihjatc3  41759  dihmeetlem9N  41761  dihmeetlem13N  41765  dihmeetlem20N  41772  dih1dimatlem0  41774  mapdpglem24  42150  mapdpglem32  42151  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  mapdh9aOLDN  42236  hdmap14lem6  42319  sn-addlid  42836  mzpsubst  43180  pellexlem5  43261  pellex  43263  pell14qrexpclnn0  43294  pellfundex  43314  qirropth  43336  monotuz  43369  congtr  43393  congmul  43395  congsub  43398  mzpcong  43400  fzmaxdif  43409  jm2.15nn0  43431  idomsubgmo  43621  iunrelexpmin1  44135  iunrelexpmin2  44139  trclimalb2  44153  mnringmulrcld  44655  fourierdlem42  46577  fourierdlem48  46582  fourierdlem80  46614  smfaddlem1  47191  prmdvdsfmtnof1lem1  48047  uhgrimisgrgric  48407  uspgropssxp  48620  lidldomn1  48707  rngccatidALTV  48748  coe1sclmulval  48861  lincdifsn  48900  seposep  49401  iscnrm3rlem8  49422  iscnrm3llem2  49425