Theorem simp2l 1197

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp12l  1284  simp22l  1290  simp32l  1296  fsnunf  7039  f1oiso2  7203  fpr3g  8072  omeulem2  8376  uniinqs  8544  unxpdomlem3  8958  gruina  10505  dedekind  11068  addid2  11088  subaddmulsub  11368  dmdcan  11615  xaddass  12912  xaddass2  12913  xlt2add  12923  xmulasslem3  12949  xadddi2  12960  xadddi2r  12961  expaddzlem  13754  expaddz  13755  expmulz  13757  expdiv  13762  expmordi  13813  modexp  13881  pfxeq  14337  ccatopth2  14358  swrdco  14478  o1add  15251  o1mul  15252  o1sub  15253  fsumsplitsnun  15395  ntrivcvgmul  15542  prmexpb  16353  pcpremul  16472  pcdiv  16481  pcqmul  16482  pcqdiv  16486  4sqlem12  16585  f1ocpbllem  17152  ercpbl  17177  erlecpbl  17178  latjlej12  18088  latmlem12  18104  latj4  18122  latj4rot  18123  gsumsgrpccat  18393  gsmsymgreqlem2  18954  symgsssg  18990  symgfisg  18991  mndodcong  19065  cmn4  19321  ablsub4  19329  abladdsub4  19330  lsm4  19376  abvdom  20013  abvres  20014  abvtrivd  20015  lspsnvs  20291  lspsneu  20300  lspfixed  20305  lspexch  20306  lsmcv  20318  lspsolvlem  20319  coe1sclmulfv  21364  matvscacell  21493  m1detdiag  21654  cramerimplem3  21742  cnprest  22348  hausnei2  22412  isreg2  22436  cmpcld  22461  llyrest  22544  nllyrest  22545  elptr  22632  basqtop  22770  hausflimlem  23038  tmdgsum  23154  utop2nei  23310  trcfilu  23354  ssblps  23483  ssbl  23484  prdsxmslem2  23591  tgqioo  23869  metnrm  23931  bndth  24027  ncvspi  24225  ncvs1  24226  cph2ass  24282  lmmbr2  24328  iscau3  24347  bcthlem5  24397  ovolunlem2  24567  dvres2  24981  dvfsumlem2  25096  plyadd  25283  plymul  25284  coeeu  25291  coemullem  25316  aalioulem4  25400  mulcxp  25745  cxplea  25756  cxple2  25757  cxplt2  25758  cxpcn3lem  25805  angcan  25857  ang180lem5  25868  divsqrtsumlem  26034  logexprlim  26278  dchrvmasumlema  26553  dchrisum0lema  26567  logdivsum  26586  log2sumbnd  26597  abvcxp  26668  padicabv  26683  tghilberti2  26903  brbtwn2  27176  axcontlem4  27238  axcontlem8  27242  clwlkl1loop  28052  clwwlknonex2lem2  28373  clwlknon2num  28633  numclwlk1lem2  28635  chscllem4  29903  orngmul  31404  measxun2  32078  measun  32079  mbfmco2  32132  probun  32286  satfv1fvfmla1  33285  nolesgn2ores  33802  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem2  33839  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd1lem6  33843  noinffv  33851  noinfres  33852  noinfbnd1lem1  33853  noinfbnd1lem2  33854  noinfbnd1lem4  33856  noinfbnd1lem6  33858  nosupinfsep  33862  scutbdaylt  33939  cgrcomim  34218  cgrcoml  34225  cgrcomr  34226  cgrdegen  34233  btwnintr  34248  btwnexch3  34249  btwnouttr2  34251  btwnouttr  34253  btwnexch  34254  btwndiff  34256  lineid  34312  idinside  34313  btwnconn1lem7  34322  btwnconn1lem8  34323  btwnconn1lem9  34324  btwnconn1lem12  34327  btwnconn1lem14  34329  btwnconn3  34332  midofsegid  34333  segcon2  34334  brsegle2  34338  btwnoutside  34354  outsideoftr  34358  outsideofeu  34360  linethru  34382  cnres2  35848  heibor  35906  lsmsat  36949  lkrlsp  37043  lkrlsp2  37044  lkrlsp3  37045  latm4  37174  omlspjN  37202  hlatj4  37315  4noncolr3  37394  4noncolr2  37395  4noncolr1  37396  athgt  37397  3dimlem3a  37401  3dimlem4a  37404  3dimlem4  37405  3dimlem4OLDN  37406  3dim3  37410  1cvratex  37414  hlatexch4  37422  3atlem4  37427  atcvrlln2  37460  atcvrlln  37461  lplnnlelln  37484  lvoli2  37522  lvolnlelln  37525  lvolnlelpln  37526  4atlem11b  37549  4atlem12b  37552  2lplnja  37560  2lplnj  37561  dalemyeo  37573  dath2  37678  lncvrat  37723  cdlemblem  37734  cdlemb  37735  elpaddri  37743  padd4N  37781  llnmod2i2  37804  llnexchb2  37810  dalawlem1  37812  dalawlem2  37813  pclfinN  37841  osumcllem6N  37902  pexmidlem3N  37913  lhp2lt  37942  lhp2at0  37973  lhp2atnle  37974  lhp2atne  37975  lhp2at0nle  37976  lhp2at0ne  37977  lhpelim  37978  lhpmod2i2  37979  lhpmod6i1  37980  lhple  37983  lhpat  37984  lhpat3  37987  ltrncoelN  38084  ltrncoat  38085  ltrncnv  38087  trlat  38110  trl0  38111  ltrnnidn  38115  trlnid  38120  cdlemd7  38145  cdleme0b  38153  cdleme0c  38154  cdleme0fN  38159  cdleme02N  38163  cdleme0ex1N  38164  cdleme0ex2N  38165  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme8  38191  cdleme11a  38201  cdleme17c  38229  cdleme22gb  38235  cdlemeda  38239  cdleme20k  38260  cdleme21a  38266  cdleme21d  38271  cdleme22f2  38288  cdleme22g  38289  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme24  38293  cdleme28  38314  cdlemefrs32fva1  38342  cdlemefr32sn2aw  38345  cdlemefs32sn1aw  38355  cdleme41sn3a  38374  cdleme32fva  38378  cdleme32fva1  38379  cdleme35a  38389  cdleme35b  38391  cdleme35c  38392  cdleme35f  38395  cdleme39a  38406  cdleme42a  38412  cdleme42c  38413  cdleme42b  38419  cdleme42e  38420  cdleme42f  38421  cdleme42g  38422  cdleme42h  38423  cdleme43bN  38431  cdleme46f2g2  38434  cdleme17d2  38436  cdleme17d4  38438  cdleme48fv  38440  cdleme48fvg  38441  cdleme4gfv  38448  cdlemeg46c  38454  cdlemeg46nlpq  38458  cdlemeg46gfre  38473  cdleme48d  38476  cdlemeg49lebilem  38480  cdleme50trn2  38492  cdleme50ltrn  38498  cdleme  38501  cdlemf1  38502  cdlemf  38504  trlord  38510  ltrniotacnvval  38523  ltrniotavalbN  38525  cdlemg1cex  38529  cdlemg2dN  38531  cdlemg2ce  38533  cdlemg2fvlem  38535  cdlemg2idN  38537  cdlemg2kq  38543  cdlemg2l  38544  cdlemg2m  38545  cdlemg4b2  38551  cdlemg7fvN  38565  cdlemg8a  38568  cdlemg10bALTN  38577  cdlemg11aq  38579  cdlemg12d  38587  cdlemg13a  38592  cdlemg13  38593  cdlemg14f  38594  cdlemg14g  38595  cdlemg17a  38602  cdlemg17b  38603  cdlemg27a  38633  cdlemg31b0N  38635  cdlemg31a  38638  cdlemg31b  38639  cdlemg31c  38640  ltrnco  38660  trlcoabs  38662  trlcoabs2N  38663  trlcocnvat  38665  trlconid  38666  trlcolem  38667  trlcone  38669  cdlemg42  38670  cdlemg43  38671  cdlemg46  38676  cdlemg47  38677  tendoeq1  38705  tendoco2  38709  tendoplco2  38720  tendopltp  38721  cdlemh1  38756  cdlemh2  38757  cdlemi1  38759  cdlemi  38761  cdlemk1  38772  cdlemk2  38773  cdlemk3  38774  cdlemk4  38775  cdlemk8  38779  cdlemk9  38780  cdlemk9bN  38781  cdlemk31  38837  cdlemk32  38838  cdlemk28-3  38849  cdlemk19u  38911  cdlemk56w  38914  tendoex  38916  erngdvlem4  38932  erngdvlem4-rN  38940  dia11N  38989  dib11N  39101  cdlemn6  39143  cdlemn7  39144  cdlemn8  39145  cdlemn9  39146  dihordlem6  39154  dihordlem7  39155  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord2pre  39166  dihord2pre2  39167  dihlsscpre  39175  dihvalcq2  39188  dihopelvalcpre  39189  dihord4  39199  dihord6b  39201  dihmeetlem1N  39231  dihglblem3N  39236  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetcN  39243  dihmeetbclemN  39245  dihmeetlem4preN  39247  dihjatc1  39252  dihjatc2N  39253  dihjatc3  39254  dihmeetlem9N  39256  dihmeetlem13N  39260  dihmeetlem20N  39267  dih1dimatlem0  39269  mapdpglem24  39645  mapdpglem32  39646  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  mapdh9aOLDN  39731  hdmap14lem6  39814  nnadddir  40221  sn-addid2  40308  mzpsubst  40486  pellexlem5  40571  pellex  40573  pell14qrexpclnn0  40604  pellfundex  40624  qirropth  40646  monotuz  40679  congtr  40703  congmul  40705  congsub  40708  mzpcong  40710  fzmaxdif  40719  jm2.15nn0  40741  idomsubgmo  40939  iunrelexpmin1  41205  iunrelexpmin2  41209  trclimalb2  41223  mnringmulrcld  41735  fourierdlem42  43580  fourierdlem48  43585  fourierdlem80  43617  smfaddlem1  44185  prmdvdsfmtnof1lem1  44924  uspgropssxp  45194  lidldomn1  45367  rngccatidALTV  45435  coe1sclmulval  45614  lincdifsn  45653  seposep  46107  iscnrm3rlem8  46129  iscnrm3llem2  46132