Theorem simp2l 1200

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

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

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 1088

This theorem is referenced by:  simp12l  1287  simp22l  1293  simp32l  1299  fsnunf  7131  f1oiso2  7298  fpr3g  8227  omeulem2  8510  uniinqs  8734  unxpdomlem3  9158  gruina  10729  dedekind  11296  addlid  11316  subaddmulsub  11600  dmdcan  11851  xaddass  13164  xaddass2  13165  xlt2add  13175  xmulasslem3  13201  xadddi2  13212  xadddi2r  13213  expaddzlem  14028  expaddz  14029  expmulz  14031  expdiv  14036  expmordi  14090  modexp  14161  pfxeq  14619  ccatopth2  14640  swrdco  14760  o1add  15537  o1mul  15538  o1sub  15539  fsumsplitsnun  15678  ntrivcvgmul  15825  prmexpb  16646  pcpremul  16771  pcdiv  16780  pcqmul  16781  pcqdiv  16785  4sqlem12  16884  f1ocpbllem  17445  ercpbl  17470  erlecpbl  17471  latjlej12  18378  latmlem12  18394  latj4  18412  latj4rot  18413  gsumsgrpccat  18765  gsmsymgreqlem2  19360  symgsssg  19396  symgfisg  19397  mndodcong  19471  cmn4  19730  ablsub4  19739  abladdsub4  19740  lsm4  19789  abvdom  20763  abvres  20764  abvtrivd  20765  orngmul  20798  lspsnvs  21069  lspsneu  21078  lspfixed  21083  lspexch  21084  lsmcv  21096  lspsolvlem  21097  ring2idlqus1  21274  coe1sclmulfv  22225  matvscacell  22380  m1detdiag  22541  cramerimplem3  22629  cnprest  23233  hausnei2  23297  isreg2  23321  cmpcld  23346  llyrest  23429  nllyrest  23430  elptr  23517  basqtop  23655  hausflimlem  23923  tmdgsum  24039  utop2nei  24194  trcfilu  24237  ssblps  24366  ssbl  24367  prdsxmslem2  24473  tgqioo  24744  metnrm  24807  bndth  24913  ncvspi  25112  ncvs1  25113  cph2ass  25169  lmmbr2  25215  iscau3  25234  bcthlem5  25284  ovolunlem2  25455  dvres2  25869  dvfsumlem2  25989  dvfsumlem2OLD  25990  plyadd  26178  plymul  26179  coeeu  26186  coemullem  26211  aalioulem4  26299  mulcxp  26650  cxplea  26661  cxple2  26662  cxplt2  26663  cxpcn3lem  26713  angcan  26768  ang180lem5  26779  divsqrtsumlem  26946  logexprlim  27192  dchrvmasumlema  27467  dchrisum0lema  27481  logdivsum  27500  log2sumbnd  27511  abvcxp  27582  padicabv  27597  nolesgn2ores  27640  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem2  27677  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd1lem6  27681  noinffv  27689  noinfres  27690  noinfbnd1lem1  27691  noinfbnd1lem2  27692  noinfbnd1lem4  27694  noinfbnd1lem6  27696  nosupinfsep  27700  cutbdaylt  27794  expsgt0  28433  bdayfinbndlem1  28463  tghilberti2  28710  brbtwn2  28978  axcontlem4  29040  axcontlem8  29044  clwlkl1loop  29856  clwwlknonex2lem2  30183  clwlknon2num  30443  numclwlk1lem2  30445  chscllem4  31715  measxun2  34367  measun  34368  mbfmco2  34422  probun  34576  satfv1fvfmla1  35617  cgrcomim  36183  cgrcoml  36190  cgrcomr  36191  cgrdegen  36198  btwnintr  36213  btwnexch3  36214  btwnouttr2  36216  btwnouttr  36218  btwnexch  36219  btwndiff  36221  lineid  36277  idinside  36278  btwnconn1lem7  36287  btwnconn1lem8  36288  btwnconn1lem9  36289  btwnconn1lem12  36292  btwnconn1lem14  36294  btwnconn3  36297  midofsegid  36298  segcon2  36299  brsegle2  36303  btwnoutside  36319  outsideoftr  36323  outsideofeu  36325  linethru  36347  cnres2  37960  heibor  38018  lsmsat  39264  lkrlsp  39358  lkrlsp2  39359  lkrlsp3  39360  latm4  39489  omlspjN  39517  hlatj4  39630  4noncolr3  39709  4noncolr2  39710  4noncolr1  39711  athgt  39712  3dimlem3a  39716  3dimlem4a  39719  3dimlem4  39720  3dimlem4OLDN  39721  3dim3  39725  1cvratex  39729  hlatexch4  39737  3atlem4  39742  atcvrlln2  39775  atcvrlln  39776  lplnnlelln  39799  lvoli2  39837  lvolnlelln  39840  lvolnlelpln  39841  4atlem11b  39864  4atlem12b  39867  2lplnja  39875  2lplnj  39876  dalemyeo  39888  dath2  39993  lncvrat  40038  cdlemblem  40049  cdlemb  40050  elpaddri  40058  padd4N  40096  llnmod2i2  40119  llnexchb2  40125  dalawlem1  40127  dalawlem2  40128  pclfinN  40156  osumcllem6N  40217  pexmidlem3N  40228  lhp2lt  40257  lhp2at0  40288  lhp2atnle  40289  lhp2atne  40290  lhp2at0nle  40291  lhp2at0ne  40292  lhpelim  40293  lhpmod2i2  40294  lhpmod6i1  40295  lhple  40298  lhpat  40299  lhpat3  40302  ltrncoelN  40399  ltrncoat  40400  ltrncnv  40402  trlat  40425  trl0  40426  ltrnnidn  40430  trlnid  40435  cdlemd7  40460  cdleme0b  40468  cdleme0c  40469  cdleme0fN  40474  cdleme02N  40478  cdleme0ex1N  40479  cdleme0ex2N  40480  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme8  40506  cdleme11a  40516  cdleme17c  40544  cdleme22gb  40550  cdlemeda  40554  cdleme20k  40575  cdleme21a  40581  cdleme21d  40586  cdleme22f2  40603  cdleme22g  40604  cdleme23a  40605  cdleme23b  40606  cdleme23c  40607  cdleme24  40608  cdleme28  40629  cdlemefrs32fva1  40657  cdlemefr32sn2aw  40660  cdlemefs32sn1aw  40670  cdleme41sn3a  40689  cdleme32fva  40693  cdleme32fva1  40694  cdleme35a  40704  cdleme35b  40706  cdleme35c  40707  cdleme35f  40710  cdleme39a  40721  cdleme42a  40727  cdleme42c  40728  cdleme42b  40734  cdleme42e  40735  cdleme42f  40736  cdleme42g  40737  cdleme42h  40738  cdleme43bN  40746  cdleme46f2g2  40749  cdleme17d2  40751  cdleme17d4  40753  cdleme48fv  40755  cdleme48fvg  40756  cdleme4gfv  40763  cdlemeg46c  40769  cdlemeg46nlpq  40773  cdlemeg46gfre  40788  cdleme48d  40791  cdlemeg49lebilem  40795  cdleme50trn2  40807  cdleme50ltrn  40813  cdleme  40816  cdlemf1  40817  cdlemf  40819  trlord  40825  ltrniotacnvval  40838  ltrniotavalbN  40840  cdlemg1cex  40844  cdlemg2dN  40846  cdlemg2ce  40848  cdlemg2fvlem  40850  cdlemg2idN  40852  cdlemg2kq  40858  cdlemg2l  40859  cdlemg2m  40860  cdlemg4b2  40866  cdlemg7fvN  40880  cdlemg8a  40883  cdlemg10bALTN  40892  cdlemg11aq  40894  cdlemg12d  40902  cdlemg13a  40907  cdlemg13  40908  cdlemg14f  40909  cdlemg14g  40910  cdlemg17a  40917  cdlemg17b  40918  cdlemg27a  40948  cdlemg31b0N  40950  cdlemg31a  40953  cdlemg31b  40954  cdlemg31c  40955  ltrnco  40975  trlcoabs  40977  trlcoabs2N  40978  trlcocnvat  40980  trlconid  40981  trlcolem  40982  trlcone  40984  cdlemg42  40985  cdlemg43  40986  cdlemg46  40991  cdlemg47  40992  tendoeq1  41020  tendoco2  41024  tendoplco2  41035  tendopltp  41036  cdlemh1  41071  cdlemh2  41072  cdlemi1  41074  cdlemi  41076  cdlemk1  41087  cdlemk2  41088  cdlemk3  41089  cdlemk4  41090  cdlemk8  41094  cdlemk9  41095  cdlemk9bN  41096  cdlemk31  41152  cdlemk32  41153  cdlemk28-3  41164  cdlemk19u  41226  cdlemk56w  41229  tendoex  41231  erngdvlem4  41247  erngdvlem4-rN  41255  dia11N  41304  dib11N  41416  cdlemn6  41458  cdlemn7  41459  cdlemn8  41460  cdlemn9  41461  dihordlem6  41469  dihordlem7  41470  dihord1  41474  dihord2a  41475  dihord2b  41476  dihord2pre  41481  dihord2pre2  41482  dihlsscpre  41490  dihvalcq2  41503  dihopelvalcpre  41504  dihord4  41514  dihord6b  41516  dihmeetlem1N  41546  dihglblem3N  41551  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetcN  41558  dihmeetbclemN  41560  dihmeetlem4preN  41562  dihjatc1  41567  dihjatc2N  41568  dihjatc3  41569  dihmeetlem9N  41571  dihmeetlem13N  41575  dihmeetlem20N  41582  dih1dimatlem0  41584  mapdpglem24  41960  mapdpglem32  41961  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  mapdh9aOLDN  42046  hdmap14lem6  42129  nnadddir  42521  sn-addlid  42655  mzpsubst  42986  pellexlem5  43071  pellex  43073  pell14qrexpclnn0  43104  pellfundex  43124  qirropth  43146  monotuz  43179  congtr  43203  congmul  43205  congsub  43208  mzpcong  43210  fzmaxdif  43219  jm2.15nn0  43241  idomsubgmo  43431  iunrelexpmin1  43945  iunrelexpmin2  43949  trclimalb2  43963  mnringmulrcld  44465  fourierdlem42  46389  fourierdlem48  46394  fourierdlem80  46426  smfaddlem1  47003  prmdvdsfmtnof1lem1  47826  uhgrimisgrgric  48173  uspgropssxp  48386  lidldomn1  48473  rngccatidALTV  48514  coe1sclmulval  48627  lincdifsn  48666  seposep  49167  iscnrm3rlem8  49188  iscnrm3llem2  49191