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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  simp12l  1288  simp22l  1294  simp32l  1300  fsnunf  6978  f1oiso2  7139  fpr3g  8004  omeulem2  8289  uniinqs  8457  unxpdomlem3  8860  gruina  10397  dedekind  10960  addid2  10980  subaddmulsub  11260  dmdcan  11507  xaddass  12804  xaddass2  12805  xlt2add  12815  xmulasslem3  12841  xadddi2  12852  xadddi2r  12853  expaddzlem  13643  expaddz  13644  expmulz  13646  expdiv  13651  expmordi  13702  modexp  13770  pfxeq  14226  ccatopth2  14247  swrdco  14367  o1add  15140  o1mul  15141  o1sub  15142  fsumsplitsnun  15282  ntrivcvgmul  15429  prmexpb  16240  pcpremul  16359  pcdiv  16368  pcqmul  16369  pcqdiv  16373  4sqlem12  16472  f1ocpbllem  16983  ercpbl  17008  erlecpbl  17009  latjlej12  17915  latmlem12  17931  latj4  17949  latj4rot  17950  gsumsgrpccat  18220  gsmsymgreqlem2  18777  symgsssg  18813  symgfisg  18814  mndodcong  18888  cmn4  19144  ablsub4  19152  abladdsub4  19153  lsm4  19199  abvdom  19828  abvres  19829  abvtrivd  19830  lspsnvs  20105  lspsneu  20114  lspfixed  20119  lspexch  20120  lsmcv  20132  lspsolvlem  20133  coe1sclmulfv  21158  matvscacell  21287  m1detdiag  21448  cramerimplem3  21536  cnprest  22140  hausnei2  22204  isreg2  22228  cmpcld  22253  llyrest  22336  nllyrest  22337  elptr  22424  basqtop  22562  hausflimlem  22830  tmdgsum  22946  utop2nei  23102  trcfilu  23145  ssblps  23274  ssbl  23275  prdsxmslem2  23381  tgqioo  23651  metnrm  23713  bndth  23809  ncvspi  24007  ncvs1  24008  cph2ass  24064  lmmbr2  24110  iscau3  24129  bcthlem5  24179  ovolunlem2  24349  dvres2  24763  dvfsumlem2  24878  plyadd  25065  plymul  25066  coeeu  25073  coemullem  25098  aalioulem4  25182  mulcxp  25527  cxplea  25538  cxple2  25539  cxplt2  25540  cxpcn3lem  25587  angcan  25639  ang180lem5  25650  divsqrtsumlem  25816  logexprlim  26060  dchrvmasumlema  26335  dchrisum0lema  26349  logdivsum  26368  log2sumbnd  26379  abvcxp  26450  padicabv  26465  tghilberti2  26683  brbtwn2  26950  axcontlem4  27012  axcontlem8  27016  clwlkl1loop  27824  clwwlknonex2lem2  28145  clwlknon2num  28405  numclwlk1lem2  28407  chscllem4  29675  orngmul  31175  measxun2  31844  measun  31845  mbfmco2  31898  probun  32052  satfv1fvfmla1  33052  nolesgn2ores  33561  nosupres  33596  nosupbnd1lem1  33597  nosupbnd1lem2  33598  nosupbnd1lem4  33600  nosupbnd1lem5  33601  nosupbnd1lem6  33602  noinffv  33610  noinfres  33611  noinfbnd1lem1  33612  noinfbnd1lem2  33613  noinfbnd1lem4  33615  noinfbnd1lem6  33617  nosupinfsep  33621  scutbdaylt  33698  cgrcomim  33977  cgrcoml  33984  cgrcomr  33985  cgrdegen  33992  btwnintr  34007  btwnexch3  34008  btwnouttr2  34010  btwnouttr  34012  btwnexch  34013  btwndiff  34015  lineid  34071  idinside  34072  btwnconn1lem7  34081  btwnconn1lem8  34082  btwnconn1lem9  34083  btwnconn1lem12  34086  btwnconn1lem14  34088  btwnconn3  34091  midofsegid  34092  segcon2  34093  brsegle2  34097  btwnoutside  34113  outsideoftr  34117  outsideofeu  34119  linethru  34141  cnres2  35607  heibor  35665  lsmsat  36708  lkrlsp  36802  lkrlsp2  36803  lkrlsp3  36804  latm4  36933  omlspjN  36961  hlatj4  37074  4noncolr3  37153  4noncolr2  37154  4noncolr1  37155  athgt  37156  3dimlem3a  37160  3dimlem4a  37163  3dimlem4  37164  3dimlem4OLDN  37165  3dim3  37169  1cvratex  37173  hlatexch4  37181  3atlem4  37186  atcvrlln2  37219  atcvrlln  37220  lplnnlelln  37243  lvoli2  37281  lvolnlelln  37284  lvolnlelpln  37285  4atlem11b  37308  4atlem12b  37311  2lplnja  37319  2lplnj  37320  dalemyeo  37332  dath2  37437  lncvrat  37482  cdlemblem  37493  cdlemb  37494  elpaddri  37502  padd4N  37540  llnmod2i2  37563  llnexchb2  37569  dalawlem1  37571  dalawlem2  37572  pclfinN  37600  osumcllem6N  37661  pexmidlem3N  37672  lhp2lt  37701  lhp2at0  37732  lhp2atnle  37733  lhp2atne  37734  lhp2at0nle  37735  lhp2at0ne  37736  lhpelim  37737  lhpmod2i2  37738  lhpmod6i1  37739  lhple  37742  lhpat  37743  lhpat3  37746  ltrncoelN  37843  ltrncoat  37844  ltrncnv  37846  trlat  37869  trl0  37870  ltrnnidn  37874  trlnid  37879  cdlemd7  37904  cdleme0b  37912  cdleme0c  37913  cdleme0fN  37918  cdleme02N  37922  cdleme0ex1N  37923  cdleme0ex2N  37924  cdleme7aa  37942  cdleme7c  37945  cdleme7d  37946  cdleme7e  37947  cdleme7ga  37948  cdleme7  37949  cdleme8  37950  cdleme11a  37960  cdleme17c  37988  cdleme22gb  37994  cdlemeda  37998  cdleme20k  38019  cdleme21a  38025  cdleme21d  38030  cdleme22f2  38047  cdleme22g  38048  cdleme23a  38049  cdleme23b  38050  cdleme23c  38051  cdleme24  38052  cdleme28  38073  cdlemefrs32fva1  38101  cdlemefr32sn2aw  38104  cdlemefs32sn1aw  38114  cdleme41sn3a  38133  cdleme32fva  38137  cdleme32fva1  38138  cdleme35a  38148  cdleme35b  38150  cdleme35c  38151  cdleme35f  38154  cdleme39a  38165  cdleme42a  38171  cdleme42c  38172  cdleme42b  38178  cdleme42e  38179  cdleme42f  38180  cdleme42g  38181  cdleme42h  38182  cdleme43bN  38190  cdleme46f2g2  38193  cdleme17d2  38195  cdleme17d4  38197  cdleme48fv  38199  cdleme48fvg  38200  cdleme4gfv  38207  cdlemeg46c  38213  cdlemeg46nlpq  38217  cdlemeg46gfre  38232  cdleme48d  38235  cdlemeg49lebilem  38239  cdleme50trn2  38251  cdleme50ltrn  38257  cdleme  38260  cdlemf1  38261  cdlemf  38263  trlord  38269  ltrniotacnvval  38282  ltrniotavalbN  38284  cdlemg1cex  38288  cdlemg2dN  38290  cdlemg2ce  38292  cdlemg2fvlem  38294  cdlemg2idN  38296  cdlemg2kq  38302  cdlemg2l  38303  cdlemg2m  38304  cdlemg4b2  38310  cdlemg7fvN  38324  cdlemg8a  38327  cdlemg10bALTN  38336  cdlemg11aq  38338  cdlemg12d  38346  cdlemg13a  38351  cdlemg13  38352  cdlemg14f  38353  cdlemg14g  38354  cdlemg17a  38361  cdlemg17b  38362  cdlemg27a  38392  cdlemg31b0N  38394  cdlemg31a  38397  cdlemg31b  38398  cdlemg31c  38399  ltrnco  38419  trlcoabs  38421  trlcoabs2N  38422  trlcocnvat  38424  trlconid  38425  trlcolem  38426  trlcone  38428  cdlemg42  38429  cdlemg43  38430  cdlemg46  38435  cdlemg47  38436  tendoeq1  38464  tendoco2  38468  tendoplco2  38479  tendopltp  38480  cdlemh1  38515  cdlemh2  38516  cdlemi1  38518  cdlemi  38520  cdlemk1  38531  cdlemk2  38532  cdlemk3  38533  cdlemk4  38534  cdlemk8  38538  cdlemk9  38539  cdlemk9bN  38540  cdlemk31  38596  cdlemk32  38597  cdlemk28-3  38608  cdlemk19u  38670  cdlemk56w  38673  tendoex  38675  erngdvlem4  38691  erngdvlem4-rN  38699  dia11N  38748  dib11N  38860  cdlemn6  38902  cdlemn7  38903  cdlemn8  38904  cdlemn9  38905  dihordlem6  38913  dihordlem7  38914  dihord1  38918  dihord2a  38919  dihord2b  38920  dihord2pre  38925  dihord2pre2  38926  dihlsscpre  38934  dihvalcq2  38947  dihopelvalcpre  38948  dihord4  38958  dihord6b  38960  dihmeetlem1N  38990  dihglblem3N  38995  dihmeetlem2N  38999  dihglbcpreN  39000  dihmeetcN  39002  dihmeetbclemN  39004  dihmeetlem4preN  39006  dihjatc1  39011  dihjatc2N  39012  dihjatc3  39013  dihmeetlem9N  39015  dihmeetlem13N  39019  dihmeetlem20N  39026  dih1dimatlem0  39028  mapdpglem24  39404  mapdpglem32  39405  baerlem3lem2  39410  baerlem5alem2  39411  baerlem5blem2  39412  mapdh9aOLDN  39490  hdmap14lem6  39573  nnadddir  39948  sn-addid2  40036  mzpsubst  40214  pellexlem5  40299  pellex  40301  pell14qrexpclnn0  40332  pellfundex  40352  qirropth  40374  monotuz  40407  congtr  40431  congmul  40433  congsub  40436  mzpcong  40438  fzmaxdif  40447  jm2.15nn0  40469  idomsubgmo  40667  iunrelexpmin1  40934  iunrelexpmin2  40938  trclimalb2  40952  mnringmulrcld  41460  fourierdlem42  43308  fourierdlem48  43313  fourierdlem80  43345  smfaddlem1  43913  prmdvdsfmtnof1lem1  44652  uspgropssxp  44922  lidldomn1  45095  rngccatidALTV  45163  coe1sclmulval  45342  lincdifsn  45381  seposep  45835  iscnrm3rlem8  45857  iscnrm3llem2  45860