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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  simp12l  1305  simp22l  1311  simp32l  1317  fsnunf  7185  f1oiso2  7352  fpr3g  8283  omeulem2  8569  uniinqs  8796  unxpdomlem3  9219  gruina  10804  dedekind  11374  addlid  11394  subaddmulsub  11678  dmdcan  11926  nnadddir  12293  xaddass  13276  xaddass2  13277  xlt2add  13287  xmulasslem3  13313  xadddi2  13324  xadddi2r  13325  expaddzlem  14143  expaddz  14144  expmulz  14146  expdiv  14151  expmordi  14205  modexp  14276  pfxeq  14735  ccatopth2  14756  swrdco  14876  o1add  15667  o1mul  15668  o1sub  15669  fsumsplitsnun  15808  ntrivcvgmul  15958  prmexpb  16779  pcpremul  16904  pcdiv  16913  pcqmul  16914  pcqdiv  16918  4sqlem12  17017  f1ocpbllem  17579  ercpbl  17604  erlecpbl  17605  latjlej12  18512  latmlem12  18528  latj4  18546  latj4rot  18547  gsumsgrpccat  18900  gsmsymgreqlem2  19502  symgsssg  19538  symgfisg  19539  mndodcong  19613  cmn4  19872  ablsub4  19881  abladdsub4  19882  lsm4  19931  abvdom  20914  abvres  20915  abvtrivd  20916  orngmul  20949  lspsnvs  21219  lspsneu  21228  lspfixed  21233  lspexch  21234  lsmcv  21246  lspsolvlem  21247  ring2idlqus1  21440  coe1sclmulfv  22425  matvscacell  22574  m1detdiag  22735  cramerimplem3  22823  cnprest  23427  hausnei2  23491  isreg2  23515  cmpcld  23540  llyrest  23623  nllyrest  23624  elptr  23711  basqtop  23849  hausflimlem  24117  tmdgsum  24233  utop2nei  24388  trcfilu  24431  ssblps  24560  ssbl  24561  prdsxmslem2  24667  tgqioo  24938  metnrm  25001  bndth  25098  ncvspi  25296  ncvs1  25297  cph2ass  25353  lmmbr2  25399  iscau3  25418  bcthlem5  25468  ovolunlem2  25638  dvres2  26052  dvfsumlem2  26167  plyadd  26355  plymul  26356  coeeu  26363  coemullem  26388  aalioulem4  26479  mulcxp  26831  cxplea  26842  cxple2  26843  cxplt2  26844  cxpcn3lem  26893  angcan  26948  ang180lem5  26959  divsqrtsumlem  27125  logexprlim  27370  dchrvmasumlema  27645  dchrisum0lema  27659  logdivsum  27678  log2sumbnd  27689  abvcxp  27760  padicabv  27775  nolesgn2ores  27817  nosupres  27852  nosupbnd1lem1  27853  nosupbnd1lem2  27854  nosupbnd1lem4  27856  nosupbnd1lem5  27857  nosupbnd1lem6  27858  noinffv  27866  noinfres  27867  noinfbnd1lem1  27868  noinfbnd1lem2  27869  noinfbnd1lem4  27871  noinfbnd1lem6  27873  nosupinfsep  27877  cutbdaylt  27972  expsgt0  28611  bdayfinbndlem1  28641  tghilberti2  28892  brbtwn2  29236  axcontlem4  29298  axcontlem8  29302  clwlkl1loop  30113  clwwlknonex2lem2  30440  clwlknon2num  30700  numclwlk1lem2  30702  chscllem4  31973  measxun2  34581  measun  34582  mbfmco2  34636  probun  34790  satfv1fvfmla1  35896  cgrcomim  36462  cgrcoml  36469  cgrcomr  36470  cgrdegen  36477  btwnintr  36492  btwnexch3  36493  btwnouttr2  36495  btwnouttr  36497  btwnexch  36498  btwndiff  36500  lineid  36556  idinside  36557  btwnconn1lem7  36566  btwnconn1lem8  36567  btwnconn1lem9  36568  btwnconn1lem12  36571  btwnconn1lem14  36573  btwnconn3  36576  midofsegid  36577  segcon2  36578  brsegle2  36582  btwnoutside  36598  outsideoftr  36602  outsideofeu  36604  linethru  36626  cnres2  38395  heibor  38453  lsmsat  39763  lkrlsp  39857  lkrlsp2  39858  lkrlsp3  39859  latm4  39988  omlspjN  40016  hlatj4  40129  4noncolr3  40208  4noncolr2  40209  4noncolr1  40210  athgt  40211  3dimlem3a  40215  3dimlem4a  40218  3dimlem4  40219  3dimlem4OLDN  40220  3dim3  40224  1cvratex  40228  hlatexch4  40236  3atlem4  40241  atcvrlln2  40274  atcvrlln  40275  lplnnlelln  40298  lvoli2  40336  lvolnlelln  40339  lvolnlelpln  40340  4atlem11b  40363  4atlem12b  40366  2lplnja  40374  2lplnj  40375  dalemyeo  40387  dath2  40492  lncvrat  40537  cdlemblem  40548  cdlemb  40549  elpaddri  40557  padd4N  40595  llnmod2i2  40618  llnexchb2  40624  dalawlem1  40626  dalawlem2  40627  pclfinN  40655  osumcllem6N  40716  pexmidlem3N  40727  lhp2lt  40756  lhp2at0  40787  lhp2atnle  40788  lhp2atne  40789  lhp2at0nle  40790  lhp2at0ne  40791  lhpelim  40792  lhpmod2i2  40793  lhpmod6i1  40794  lhple  40797  lhpat  40798  lhpat3  40801  ltrncoelN  40898  ltrncoat  40899  ltrncnv  40901  trlat  40924  trl0  40925  ltrnnidn  40929  trlnid  40934  cdlemd7  40959  cdleme0b  40967  cdleme0c  40968  cdleme0fN  40973  cdleme02N  40977  cdleme0ex1N  40978  cdleme0ex2N  40979  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme8  41005  cdleme11a  41015  cdleme17c  41043  cdleme22gb  41049  cdlemeda  41053  cdleme20k  41074  cdleme21a  41080  cdleme21d  41085  cdleme22f2  41102  cdleme22g  41103  cdleme23a  41104  cdleme23b  41105  cdleme23c  41106  cdleme24  41107  cdleme28  41128  cdlemefrs32fva1  41156  cdlemefr32sn2aw  41159  cdlemefs32sn1aw  41169  cdleme41sn3a  41188  cdleme32fva  41192  cdleme32fva1  41193  cdleme35a  41203  cdleme35b  41205  cdleme35c  41206  cdleme35f  41209  cdleme39a  41220  cdleme42a  41226  cdleme42c  41227  cdleme42b  41233  cdleme42e  41234  cdleme42f  41235  cdleme42g  41236  cdleme42h  41237  cdleme43bN  41245  cdleme46f2g2  41248  cdleme17d2  41250  cdleme17d4  41252  cdleme48fv  41254  cdleme48fvg  41255  cdleme4gfv  41262  cdlemeg46c  41268  cdlemeg46nlpq  41272  cdlemeg46gfre  41287  cdleme48d  41290  cdlemeg49lebilem  41294  cdleme50trn2  41306  cdleme50ltrn  41312  cdleme  41315  cdlemf1  41316  cdlemf  41318  trlord  41324  ltrniotacnvval  41337  ltrniotavalbN  41339  cdlemg1cex  41343  cdlemg2dN  41345  cdlemg2ce  41347  cdlemg2fvlem  41349  cdlemg2idN  41351  cdlemg2kq  41357  cdlemg2l  41358  cdlemg2m  41359  cdlemg4b2  41365  cdlemg7fvN  41379  cdlemg8a  41382  cdlemg10bALTN  41391  cdlemg11aq  41393  cdlemg12d  41401  cdlemg13a  41406  cdlemg13  41407  cdlemg14f  41408  cdlemg14g  41409  cdlemg17a  41416  cdlemg17b  41417  cdlemg27a  41447  cdlemg31b0N  41449  cdlemg31a  41452  cdlemg31b  41453  cdlemg31c  41454  ltrnco  41474  trlcoabs  41476  trlcoabs2N  41477  trlcocnvat  41479  trlconid  41480  trlcolem  41481  trlcone  41483  cdlemg42  41484  cdlemg43  41485  cdlemg46  41490  cdlemg47  41491  tendoeq1  41519  tendoco2  41523  tendoplco2  41534  tendopltp  41535  cdlemh1  41570  cdlemh2  41571  cdlemi1  41573  cdlemi  41575  cdlemk1  41586  cdlemk2  41587  cdlemk3  41588  cdlemk4  41589  cdlemk8  41593  cdlemk9  41594  cdlemk9bN  41595  cdlemk31  41651  cdlemk32  41652  cdlemk28-3  41663  cdlemk19u  41725  cdlemk56w  41728  tendoex  41730  erngdvlem4  41746  erngdvlem4-rN  41754  dia11N  41803  dib11N  41915  cdlemn6  41957  cdlemn7  41958  cdlemn8  41959  cdlemn9  41960  dihordlem6  41968  dihordlem7  41969  dihord1  41973  dihord2a  41974  dihord2b  41975  dihord2pre  41980  dihord2pre2  41981  dihlsscpre  41989  dihvalcq2  42002  dihopelvalcpre  42003  dihord4  42013  dihord6b  42015  dihmeetlem1N  42045  dihglblem3N  42050  dihmeetlem2N  42054  dihglbcpreN  42055  dihmeetcN  42057  dihmeetbclemN  42059  dihmeetlem4preN  42061  dihjatc1  42066  dihjatc2N  42067  dihjatc3  42068  dihmeetlem9N  42070  dihmeetlem13N  42074  dihmeetlem20N  42081  dih1dimatlem0  42083  mapdpglem24  42459  mapdpglem32  42460  baerlem3lem2  42465  baerlem5alem2  42466  baerlem5blem2  42467  mapdh9aOLDN  42545  hdmap14lem6  42628  sn-addlid  43146  mzpsubst  43462  pellexlem5  43543  pellex  43545  pell14qrexpclnn0  43576  pellfundex  43596  qirropth  43618  monotuz  43651  congtr  43675  congmul  43677  congsub  43680  mzpcong  43682  fzmaxdif  43691  jm2.15nn0  43713  idomsubgmo  43903  iunrelexpmin1  44417  iunrelexpmin2  44421  trclimalb2  44435  mnringmulrcld  44935  fourierdlem42  46846  fourierdlem48  46851  fourierdlem80  46883  smfaddlem1  47460  prmdvdsfmtnof1lem1  48319  uhgrimisgrgric  48679  uspgropssxp  48892  lidldomn1  48979  rngccatidALTV  49020  coe1sclmulval  49148  lincdifsn  49187  seposep  49687  iscnrm3rlem8  49708  iscnrm3llem2  49711