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  7190  f1resrcmplf1d  7280  f1oiso2  7361  fpr3g  8291  omeulem2  8577  uniinqs  8804  unxpdomlem3  9228  gruina  10821  dedekind  11391  addlid  11411  subaddmulsub  11695  dmdcan  11943  nnadddir  12310  xaddass  13293  xaddass2  13294  xlt2add  13304  xmulasslem3  13330  xadddi2  13341  xadddi2r  13342  expaddzlem  14161  expaddz  14162  expmulz  14164  expdiv  14169  expmordi  14223  modexp  14294  pfxeq  14757  ccatopth2  14778  swrdco  14900  o1add  15691  o1mul  15692  o1sub  15693  fsumsplitsnun  15832  ntrivcvgmul  15982  prmexpb  16803  pcpremul  16928  pcdiv  16937  pcqmul  16938  pcqdiv  16942  4sqlem12  17041  f1ocpbllem  17603  ercpbl  17628  erlecpbl  17629  latjlej12  18536  latmlem12  18552  latj4  18570  latj4rot  18571  gsumsgrpccat  18930  gsmsymgreqlem2  19532  symgsssg  19568  symgfisg  19569  mndodcong  19643  cmn4  19902  ablsub4  19911  abladdsub4  19912  lsm4  19961  abvdom  20970  abvres  20971  abvtrivd  20972  orngmul  21005  lspsnvs  21275  lspsneu  21284  lspfixed  21289  lspexch  21290  lsmcv  21302  lspsolvlem  21303  ring2idlqus1  21496  coe1sclmulfv  22481  matvscacell  22630  m1detdiag  22791  cramerimplem3  22879  cnprest  23483  hausnei2  23547  isreg2  23571  cmpcld  23596  llyrest  23679  nllyrest  23680  elptr  23767  basqtop  23905  hausflimlem  24173  tmdgsum  24289  utop2nei  24444  trcfilu  24487  ssblps  24616  ssbl  24617  prdsxmslem2  24723  tgqioo  24994  metnrm  25057  bndth  25154  ncvspi  25352  ncvs1  25353  cph2ass  25409  lmmbr2  25455  iscau3  25474  bcthlem5  25524  ovolunlem2  25694  dvres2  26108  dvfsumlem2  26223  plyadd  26411  plymul  26412  coeeu  26419  coemullem  26444  aalioulem4  26535  mulcxp  26887  cxplea  26898  cxple2  26899  cxplt2  26900  cxpcn3lem  26949  angcan  27004  ang180lem5  27015  divsqrtsumlem  27181  logexprlim  27426  dchrvmasumlema  27701  dchrisum0lema  27715  logdivsum  27734  log2sumbnd  27745  abvcxp  27816  padicabv  27831  nolesgn2ores  27873  nosupres  27908  nosupbnd1lem1  27909  nosupbnd1lem2  27910  nosupbnd1lem4  27912  nosupbnd1lem5  27913  nosupbnd1lem6  27914  noinffv  27922  noinfres  27923  noinfbnd1lem1  27924  noinfbnd1lem2  27925  noinfbnd1lem4  27927  noinfbnd1lem6  27929  nosupinfsep  27933  cutbdaylt  28028  expsgt0  28667  bdayfinbndlem1  28697  tghilberti2  28948  brbtwn2  29292  axcontlem4  29354  axcontlem8  29358  clwlkl1loop  30169  clwwlknonex2lem2  30496  clwlknon2num  30756  numclwlk1lem2  30758  chscllem4  32029  measxun2  34632  measun  34633  mbfmco2  34687  probun  34841  satfv1fvfmla1  35936  cgrcomim  36502  cgrcoml  36509  cgrcomr  36510  cgrdegen  36517  btwnintr  36532  btwnexch3  36533  btwnouttr2  36535  btwnouttr  36537  btwnexch  36538  btwndiff  36540  lineid  36596  idinside  36597  btwnconn1lem7  36606  btwnconn1lem8  36607  btwnconn1lem9  36608  btwnconn1lem12  36611  btwnconn1lem14  36613  btwnconn3  36616  midofsegid  36617  segcon2  36618  brsegle2  36622  btwnoutside  36638  outsideoftr  36642  outsideofeu  36644  linethru  36666  cnres2  38455  heibor  38513  lsmsat  39823  lkrlsp  39917  lkrlsp2  39918  lkrlsp3  39919  latm4  40048  omlspjN  40076  hlatj4  40189  4noncolr3  40268  4noncolr2  40269  4noncolr1  40270  athgt  40271  3dimlem3a  40275  3dimlem4a  40278  3dimlem4  40279  3dimlem4OLDN  40280  3dim3  40284  1cvratex  40288  hlatexch4  40296  3atlem4  40301  atcvrlln2  40334  atcvrlln  40335  lplnnlelln  40358  lvoli2  40396  lvolnlelln  40399  lvolnlelpln  40400  4atlem11b  40423  4atlem12b  40426  2lplnja  40434  2lplnj  40435  dalemyeo  40447  dath2  40552  lncvrat  40597  cdlemblem  40608  cdlemb  40609  elpaddri  40617  padd4N  40655  llnmod2i2  40678  llnexchb2  40684  dalawlem1  40686  dalawlem2  40687  pclfinN  40715  osumcllem6N  40776  pexmidlem3N  40787  lhp2lt  40816  lhp2at0  40847  lhp2atnle  40848  lhp2atne  40849  lhp2at0nle  40850  lhp2at0ne  40851  lhpelim  40852  lhpmod2i2  40853  lhpmod6i1  40854  lhple  40857  lhpat  40858  lhpat3  40861  ltrncoelN  40958  ltrncoat  40959  ltrncnv  40961  trlat  40984  trl0  40985  ltrnnidn  40989  trlnid  40994  cdlemd7  41019  cdleme0b  41027  cdleme0c  41028  cdleme0fN  41033  cdleme02N  41037  cdleme0ex1N  41038  cdleme0ex2N  41039  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme8  41065  cdleme11a  41075  cdleme17c  41103  cdleme22gb  41109  cdlemeda  41113  cdleme20k  41134  cdleme21a  41140  cdleme21d  41145  cdleme22f2  41162  cdleme22g  41163  cdleme23a  41164  cdleme23b  41165  cdleme23c  41166  cdleme24  41167  cdleme28  41188  cdlemefrs32fva1  41216  cdlemefr32sn2aw  41219  cdlemefs32sn1aw  41229  cdleme41sn3a  41248  cdleme32fva  41252  cdleme32fva1  41253  cdleme35a  41263  cdleme35b  41265  cdleme35c  41266  cdleme35f  41269  cdleme39a  41280  cdleme42a  41286  cdleme42c  41287  cdleme42b  41293  cdleme42e  41294  cdleme42f  41295  cdleme42g  41296  cdleme42h  41297  cdleme43bN  41305  cdleme46f2g2  41308  cdleme17d2  41310  cdleme17d4  41312  cdleme48fv  41314  cdleme48fvg  41315  cdleme4gfv  41322  cdlemeg46c  41328  cdlemeg46nlpq  41332  cdlemeg46gfre  41347  cdleme48d  41350  cdlemeg49lebilem  41354  cdleme50trn2  41366  cdleme50ltrn  41372  cdleme  41375  cdlemf1  41376  cdlemf  41378  trlord  41384  ltrniotacnvval  41397  ltrniotavalbN  41399  cdlemg1cex  41403  cdlemg2dN  41405  cdlemg2ce  41407  cdlemg2fvlem  41409  cdlemg2idN  41411  cdlemg2kq  41417  cdlemg2l  41418  cdlemg2m  41419  cdlemg4b2  41425  cdlemg7fvN  41439  cdlemg8a  41442  cdlemg10bALTN  41451  cdlemg11aq  41453  cdlemg12d  41461  cdlemg13a  41466  cdlemg13  41467  cdlemg14f  41468  cdlemg14g  41469  cdlemg17a  41476  cdlemg17b  41477  cdlemg27a  41507  cdlemg31b0N  41509  cdlemg31a  41512  cdlemg31b  41513  cdlemg31c  41514  ltrnco  41534  trlcoabs  41536  trlcoabs2N  41537  trlcocnvat  41539  trlconid  41540  trlcolem  41541  trlcone  41543  cdlemg42  41544  cdlemg43  41545  cdlemg46  41550  cdlemg47  41551  tendoeq1  41579  tendoco2  41583  tendoplco2  41594  tendopltp  41595  cdlemh1  41630  cdlemh2  41631  cdlemi1  41633  cdlemi  41635  cdlemk1  41646  cdlemk2  41647  cdlemk3  41648  cdlemk4  41649  cdlemk8  41653  cdlemk9  41654  cdlemk9bN  41655  cdlemk31  41711  cdlemk32  41712  cdlemk28-3  41723  cdlemk19u  41785  cdlemk56w  41788  tendoex  41790  erngdvlem4  41806  erngdvlem4-rN  41814  dia11N  41863  dib11N  41975  cdlemn6  42017  cdlemn7  42018  cdlemn8  42019  cdlemn9  42020  dihordlem6  42028  dihordlem7  42029  dihord1  42033  dihord2a  42034  dihord2b  42035  dihord2pre  42040  dihord2pre2  42041  dihlsscpre  42049  dihvalcq2  42062  dihopelvalcpre  42063  dihord4  42073  dihord6b  42075  dihmeetlem1N  42105  dihglblem3N  42110  dihmeetlem2N  42114  dihglbcpreN  42115  dihmeetcN  42117  dihmeetbclemN  42119  dihmeetlem4preN  42121  dihjatc1  42126  dihjatc2N  42127  dihjatc3  42128  dihmeetlem9N  42130  dihmeetlem13N  42134  dihmeetlem20N  42141  dih1dimatlem0  42143  mapdpglem24  42519  mapdpglem32  42520  baerlem3lem2  42525  baerlem5alem2  42526  baerlem5blem2  42527  mapdh9aOLDN  42605  hdmap14lem6  42688  sn-addlid  43206  mzpsubst  43520  pellexlem5  43601  pellex  43603  pell14qrexpclnn0  43634  pellfundex  43654  qirropth  43676  monotuz  43709  congtr  43733  congmul  43735  congsub  43738  mzpcong  43740  fzmaxdif  43749  jm2.15nn0  43771  idomsubgmo  43961  iunrelexpmin1  44475  iunrelexpmin2  44479  trclimalb2  44493  mnringmulrcld  44993  fourierdlem42  46904  fourierdlem48  46909  fourierdlem80  46941  smfaddlem1  47518  prmdvdsfmtnof1lem1  48377  uhgrimisgrgric  48737  uspgropssxp  48950  lidldomn1  49037  rngccatidALTV  49078  coe1sclmulval  49206  lincdifsn  49245  seposep  49745  iscnrm3rlem8  49766  iscnrm3llem2  49769