Theorem simp2l 1218

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp12l  1305  simp22l  1311  simp32l  1317  fsnunf  7182  f1resrcmplf1d  7271  f1oiso2  7352  fpr3g  8287  omeulem2  8575  uniinqs  8802  unxpdomlem3  9233  gruina  10884  dedekind  11454  addlid  11474  subaddmulsub  11760  dmdcan  12008  nnadddir  12375  xaddass  13360  xaddass2  13361  xlt2add  13371  xmulasslem3  13397  xadddi2  13408  xadddi2r  13409  expaddzlem  14228  expaddz  14229  expmulz  14231  expdiv  14236  expmordi  14290  modexp  14362  pfxeq  14825  ccatopth2  14846  swrdco  14968  o1add  15761  o1mul  15762  o1sub  15763  fsumsplitsnun  15901  ntrivcvgmul  16051  prmexpb  16875  pcpremul  17001  pcdiv  17010  pcqmul  17011  pcqdiv  17015  4sqlem12  17114  f1ocpbllem  17676  ercpbl  17701  erlecpbl  17702  latjlej12  18609  latmlem12  18625  latj4  18643  latj4rot  18644  gsumsgrpccat  19016  gsmsymgreqlem2  19625  symgsssg  19661  symgfisg  19662  mndodcong  19736  cmn4  19995  ablsub4  20004  abladdsub4  20005  lsm4  20054  abvdom  21067  abvres  21068  abvtrivd  21069  orngmul  21102  lspsnvs  21372  lspsneu  21381  lspfixed  21386  lspexch  21387  lsmcv  21399  lspsolvlem  21400  ring2idlqus1  21595  coe1sclmulfv  22582  matvscacell  22731  m1detdiag  22892  cramerimplem3  22983  cnprest  23587  hausnei2  23651  isreg2  23675  cmpcld  23700  llyrest  23784  nllyrest  23785  elptr  23872  basqtop  24010  hausflimlem  24278  tmdgsum  24394  utop2nei  24549  trcfilu  24592  ssblps  24721  ssbl  24722  prdsxmslem2  24828  tgqioo  25099  metnrm  25162  bndth  25259  ncvspi  25457  ncvs1  25458  cph2ass  25514  lmmbr2  25560  iscau3  25579  bcthlem5  25629  ovolunlem2  25799  dvres2  26212  dvfsumlem2  26327  plyadd  26516  plymul  26517  coeeu  26524  coemullem  26549  aalioulem4  26644  mulcxp  26995  cxplea  27006  cxple2  27007  cxplt2  27008  cxpcn3lem  27057  angcan  27112  ang180lem5  27123  divsqrtsumlem  27289  logexprlim  27534  dchrvmasumlema  27809  dchrisum0lema  27823  logdivsum  27842  log2sumbnd  27853  abvcxp  27924  padicabv  27939  nolesgn2ores  28011  nosupres  28046  nosupbnd1lem1  28047  nosupbnd1lem2  28048  nosupbnd1lem4  28050  nosupbnd1lem5  28051  nosupbnd1lem6  28052  noinffv  28060  noinfres  28061  noinfbnd1lem1  28062  noinfbnd1lem2  28063  noinfbnd1lem4  28065  noinfbnd1lem6  28067  nosupinfsep  28071  cutbdaylt  28166  expsgt0  28805  bdayfinbndlem1  28835  tghilberti2  29088  brbtwn2  29465  axcontlem4  29527  axcontlem8  29531  clwlkl1loop  30352  clwwlknonex2lem2  30681  umgr2cycllem  30728  clwlknon2num  30951  numclwlk1lem2  30953  chscllem4  32224  measxun2  34825  measun  34826  mbfmco2  34880  probun  35034  satfv1fvfmla1  36157  cgrcomim  36724  cgrcoml  36731  cgrcomr  36732  cgrdegen  36739  btwnintr  36754  btwnexch3  36755  btwnouttr2  36757  btwnouttr  36759  btwnexch  36760  btwndiff  36762  lineid  36818  idinside  36819  btwnconn1lem7  36828  btwnconn1lem8  36829  btwnconn1lem9  36830  btwnconn1lem12  36833  btwnconn1lem14  36835  btwnconn3  36838  midofsegid  36839  segcon2  36840  brsegle2  36844  btwnoutside  36860  outsideoftr  36864  outsideofeu  36866  linethru  36888  cnres2  38665  heibor  38723  lsmsat  40033  lkrlsp  40127  lkrlsp2  40128  lkrlsp3  40129  latm4  40258  omlspjN  40286  hlatj4  40399  4noncolr3  40478  4noncolr2  40479  4noncolr1  40480  athgt  40481  3dimlem3a  40485  3dimlem4a  40488  3dimlem4  40489  3dimlem4OLDN  40490  3dim3  40494  1cvratex  40498  hlatexch4  40506  3atlem4  40511  atcvrlln2  40544  atcvrlln  40545  lplnnlelln  40568  lvoli2  40606  lvolnlelln  40609  lvolnlelpln  40610  4atlem11b  40633  4atlem12b  40636  2lplnja  40644  2lplnj  40645  dalemyeo  40657  dath2  40762  lncvrat  40807  cdlemblem  40818  cdlemb  40819  elpaddri  40827  padd4N  40865  llnmod2i2  40888  llnexchb2  40894  dalawlem1  40896  dalawlem2  40897  pclfinN  40925  osumcllem6N  40986  pexmidlem3N  40997  lhp2lt  41026  lhp2at0  41057  lhp2atnle  41058  lhp2atne  41059  lhp2at0nle  41060  lhp2at0ne  41061  lhpelim  41062  lhpmod2i2  41063  lhpmod6i1  41064  lhple  41067  lhpat  41068  lhpat3  41071  ltrncoelN  41168  ltrncoat  41169  ltrncnv  41171  trlat  41194  trl0  41195  ltrnnidn  41199  trlnid  41204  cdlemd7  41229  cdleme0b  41237  cdleme0c  41238  cdleme0fN  41243  cdleme02N  41247  cdleme0ex1N  41248  cdleme0ex2N  41249  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme8  41275  cdleme11a  41285  cdleme17c  41313  cdleme22gb  41319  cdlemeda  41323  cdleme20k  41344  cdleme21a  41350  cdleme21d  41355  cdleme22f2  41372  cdleme22g  41373  cdleme23a  41374  cdleme23b  41375  cdleme23c  41376  cdleme24  41377  cdleme28  41398  cdlemefrs32fva1  41426  cdlemefr32sn2aw  41429  cdlemefs32sn1aw  41439  cdleme41sn3a  41458  cdleme32fva  41462  cdleme32fva1  41463  cdleme35a  41473  cdleme35b  41475  cdleme35c  41476  cdleme35f  41479  cdleme39a  41490  cdleme42a  41496  cdleme42c  41497  cdleme42b  41503  cdleme42e  41504  cdleme42f  41505  cdleme42g  41506  cdleme42h  41507  cdleme43bN  41515  cdleme46f2g2  41518  cdleme17d2  41520  cdleme17d4  41522  cdleme48fv  41524  cdleme48fvg  41525  cdleme4gfv  41532  cdlemeg46c  41538  cdlemeg46nlpq  41542  cdlemeg46gfre  41557  cdleme48d  41560  cdlemeg49lebilem  41564  cdleme50trn2  41576  cdleme50ltrn  41582  cdleme  41585  cdlemf1  41586  cdlemf  41588  trlord  41594  ltrniotacnvval  41607  ltrniotavalbN  41609  cdlemg1cex  41613  cdlemg2dN  41615  cdlemg2ce  41617  cdlemg2fvlem  41619  cdlemg2idN  41621  cdlemg2kq  41627  cdlemg2l  41628  cdlemg2m  41629  cdlemg4b2  41635  cdlemg7fvN  41649  cdlemg8a  41652  cdlemg10bALTN  41661  cdlemg11aq  41663  cdlemg12d  41671  cdlemg13a  41676  cdlemg13  41677  cdlemg14f  41678  cdlemg14g  41679  cdlemg17a  41686  cdlemg17b  41687  cdlemg27a  41717  cdlemg31b0N  41719  cdlemg31a  41722  cdlemg31b  41723  cdlemg31c  41724  ltrnco  41744  trlcoabs  41746  trlcoabs2N  41747  trlcocnvat  41749  trlconid  41750  trlcolem  41751  trlcone  41753  cdlemg42  41754  cdlemg43  41755  cdlemg46  41760  cdlemg47  41761  tendoeq1  41789  tendoco2  41793  tendoplco2  41804  tendopltp  41805  cdlemh1  41840  cdlemh2  41841  cdlemi1  41843  cdlemi  41845  cdlemk1  41856  cdlemk2  41857  cdlemk3  41858  cdlemk4  41859  cdlemk8  41863  cdlemk9  41864  cdlemk9bN  41865  cdlemk31  41921  cdlemk32  41922  cdlemk28-3  41933  cdlemk19u  41995  cdlemk56w  41998  tendoex  42000  erngdvlem4  42016  erngdvlem4-rN  42024  dia11N  42073  dib11N  42185  cdlemn6  42227  cdlemn7  42228  cdlemn8  42229  cdlemn9  42230  dihordlem6  42238  dihordlem7  42239  dihord1  42243  dihord2a  42244  dihord2b  42245  dihord2pre  42250  dihord2pre2  42251  dihlsscpre  42259  dihvalcq2  42272  dihopelvalcpre  42273  dihord4  42283  dihord6b  42285  dihmeetlem1N  42315  dihglblem3N  42320  dihmeetlem2N  42324  dihglbcpreN  42325  dihmeetcN  42327  dihmeetbclemN  42329  dihmeetlem4preN  42331  dihjatc1  42336  dihjatc2N  42337  dihjatc3  42338  dihmeetlem9N  42340  dihmeetlem13N  42344  dihmeetlem20N  42351  dih1dimatlem0  42353  mapdpglem24  42729  mapdpglem32  42730  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  mapdh9aOLDN  42815  hdmap14lem6  42898  sn-addlid  43423  mzpsubst  43712  pellexlem5  43793  pellex  43795  pell14qrexpclnn0  43826  pellfundex  43846  qirropth  43868  monotuz  43901  congtr  43925  congmul  43927  congsub  43930  mzpcong  43932  fzmaxdif  43941  jm2.15nn0  43963  idomsubgmo  44153  iunrelexpmin1  44667  iunrelexpmin2  44671  trclimalb2  44685  mnringmulrcld  45185  fourierdlem42  47103  fourierdlem48  47108  fourierdlem80  47140  smfaddlem1  47717  prmdvdsfmtnof1lem1  48613  uhgrimisgrgric  48973  uspgropssxp  49186  lidldomn1  49272  rngccatidALTV  49313  coe1sclmulval  49441  lincdifsn  49480  seposep  49978  iscnrm3rlem8  49999  iscnrm3llem2  50002