Theorem simp2l 1201

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

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

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 1089

This theorem is referenced by:  simp12l  1288  simp22l  1294  simp32l  1300  fsnunf  7141  f1oiso2  7308  fpr3g  8237  omeulem2  8520  uniinqs  8746  unxpdomlem3  9170  gruina  10741  dedekind  11308  addlid  11328  subaddmulsub  11612  dmdcan  11863  xaddass  13176  xaddass2  13177  xlt2add  13187  xmulasslem3  13213  xadddi2  13224  xadddi2r  13225  expaddzlem  14040  expaddz  14041  expmulz  14043  expdiv  14048  expmordi  14102  modexp  14173  pfxeq  14631  ccatopth2  14652  swrdco  14772  o1add  15549  o1mul  15550  o1sub  15551  fsumsplitsnun  15690  ntrivcvgmul  15837  prmexpb  16658  pcpremul  16783  pcdiv  16792  pcqmul  16793  pcqdiv  16797  4sqlem12  16896  f1ocpbllem  17457  ercpbl  17482  erlecpbl  17483  latjlej12  18390  latmlem12  18406  latj4  18424  latj4rot  18425  gsumsgrpccat  18777  gsmsymgreqlem2  19372  symgsssg  19408  symgfisg  19409  mndodcong  19483  cmn4  19742  ablsub4  19751  abladdsub4  19752  lsm4  19801  abvdom  20775  abvres  20776  abvtrivd  20777  orngmul  20810  lspsnvs  21081  lspsneu  21090  lspfixed  21095  lspexch  21096  lsmcv  21108  lspsolvlem  21109  ring2idlqus1  21286  coe1sclmulfv  22237  matvscacell  22392  m1detdiag  22553  cramerimplem3  22641  cnprest  23245  hausnei2  23309  isreg2  23333  cmpcld  23358  llyrest  23441  nllyrest  23442  elptr  23529  basqtop  23667  hausflimlem  23935  tmdgsum  24051  utop2nei  24206  trcfilu  24249  ssblps  24378  ssbl  24379  prdsxmslem2  24485  tgqioo  24756  metnrm  24819  bndth  24925  ncvspi  25124  ncvs1  25125  cph2ass  25181  lmmbr2  25227  iscau3  25246  bcthlem5  25296  ovolunlem2  25467  dvres2  25881  dvfsumlem2  26001  dvfsumlem2OLD  26002  plyadd  26190  plymul  26191  coeeu  26198  coemullem  26223  aalioulem4  26311  mulcxp  26662  cxplea  26673  cxple2  26674  cxplt2  26675  cxpcn3lem  26725  angcan  26780  ang180lem5  26791  divsqrtsumlem  26958  logexprlim  27204  dchrvmasumlema  27479  dchrisum0lema  27493  logdivsum  27512  log2sumbnd  27523  abvcxp  27594  padicabv  27609  nolesgn2ores  27652  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem2  27689  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd1lem6  27693  noinffv  27701  noinfres  27702  noinfbnd1lem1  27703  noinfbnd1lem2  27704  noinfbnd1lem4  27706  noinfbnd1lem6  27708  nosupinfsep  27712  cutbdaylt  27806  expsgt0  28445  bdayfinbndlem1  28475  tghilberti2  28722  brbtwn2  28990  axcontlem4  29052  axcontlem8  29056  clwlkl1loop  29868  clwwlknonex2lem2  30195  clwlknon2num  30455  numclwlk1lem2  30457  chscllem4  31727  measxun2  34387  measun  34388  mbfmco2  34442  probun  34596  satfv1fvfmla1  35636  cgrcomim  36202  cgrcoml  36209  cgrcomr  36210  cgrdegen  36217  btwnintr  36232  btwnexch3  36233  btwnouttr2  36235  btwnouttr  36237  btwnexch  36238  btwndiff  36240  lineid  36296  idinside  36297  btwnconn1lem7  36306  btwnconn1lem8  36307  btwnconn1lem9  36308  btwnconn1lem12  36311  btwnconn1lem14  36313  btwnconn3  36316  midofsegid  36317  segcon2  36318  brsegle2  36322  btwnoutside  36338  outsideoftr  36342  outsideofeu  36344  linethru  36366  cnres2  38008  heibor  38066  lsmsat  39378  lkrlsp  39472  lkrlsp2  39473  lkrlsp3  39474  latm4  39603  omlspjN  39631  hlatj4  39744  4noncolr3  39823  4noncolr2  39824  4noncolr1  39825  athgt  39826  3dimlem3a  39830  3dimlem4a  39833  3dimlem4  39834  3dimlem4OLDN  39835  3dim3  39839  1cvratex  39843  hlatexch4  39851  3atlem4  39856  atcvrlln2  39889  atcvrlln  39890  lplnnlelln  39913  lvoli2  39951  lvolnlelln  39954  lvolnlelpln  39955  4atlem11b  39978  4atlem12b  39981  2lplnja  39989  2lplnj  39990  dalemyeo  40002  dath2  40107  lncvrat  40152  cdlemblem  40163  cdlemb  40164  elpaddri  40172  padd4N  40210  llnmod2i2  40233  llnexchb2  40239  dalawlem1  40241  dalawlem2  40242  pclfinN  40270  osumcllem6N  40331  pexmidlem3N  40342  lhp2lt  40371  lhp2at0  40402  lhp2atnle  40403  lhp2atne  40404  lhp2at0nle  40405  lhp2at0ne  40406  lhpelim  40407  lhpmod2i2  40408  lhpmod6i1  40409  lhple  40412  lhpat  40413  lhpat3  40416  ltrncoelN  40513  ltrncoat  40514  ltrncnv  40516  trlat  40539  trl0  40540  ltrnnidn  40544  trlnid  40549  cdlemd7  40574  cdleme0b  40582  cdleme0c  40583  cdleme0fN  40588  cdleme02N  40592  cdleme0ex1N  40593  cdleme0ex2N  40594  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme8  40620  cdleme11a  40630  cdleme17c  40658  cdleme22gb  40664  cdlemeda  40668  cdleme20k  40689  cdleme21a  40695  cdleme21d  40700  cdleme22f2  40717  cdleme22g  40718  cdleme23a  40719  cdleme23b  40720  cdleme23c  40721  cdleme24  40722  cdleme28  40743  cdlemefrs32fva1  40771  cdlemefr32sn2aw  40774  cdlemefs32sn1aw  40784  cdleme41sn3a  40803  cdleme32fva  40807  cdleme32fva1  40808  cdleme35a  40818  cdleme35b  40820  cdleme35c  40821  cdleme35f  40824  cdleme39a  40835  cdleme42a  40841  cdleme42c  40842  cdleme42b  40848  cdleme42e  40849  cdleme42f  40850  cdleme42g  40851  cdleme42h  40852  cdleme43bN  40860  cdleme46f2g2  40863  cdleme17d2  40865  cdleme17d4  40867  cdleme48fv  40869  cdleme48fvg  40870  cdleme4gfv  40877  cdlemeg46c  40883  cdlemeg46nlpq  40887  cdlemeg46gfre  40902  cdleme48d  40905  cdlemeg49lebilem  40909  cdleme50trn2  40921  cdleme50ltrn  40927  cdleme  40930  cdlemf1  40931  cdlemf  40933  trlord  40939  ltrniotacnvval  40952  ltrniotavalbN  40954  cdlemg1cex  40958  cdlemg2dN  40960  cdlemg2ce  40962  cdlemg2fvlem  40964  cdlemg2idN  40966  cdlemg2kq  40972  cdlemg2l  40973  cdlemg2m  40974  cdlemg4b2  40980  cdlemg7fvN  40994  cdlemg8a  40997  cdlemg10bALTN  41006  cdlemg11aq  41008  cdlemg12d  41016  cdlemg13a  41021  cdlemg13  41022  cdlemg14f  41023  cdlemg14g  41024  cdlemg17a  41031  cdlemg17b  41032  cdlemg27a  41062  cdlemg31b0N  41064  cdlemg31a  41067  cdlemg31b  41068  cdlemg31c  41069  ltrnco  41089  trlcoabs  41091  trlcoabs2N  41092  trlcocnvat  41094  trlconid  41095  trlcolem  41096  trlcone  41098  cdlemg42  41099  cdlemg43  41100  cdlemg46  41105  cdlemg47  41106  tendoeq1  41134  tendoco2  41138  tendoplco2  41149  tendopltp  41150  cdlemh1  41185  cdlemh2  41186  cdlemi1  41188  cdlemi  41190  cdlemk1  41201  cdlemk2  41202  cdlemk3  41203  cdlemk4  41204  cdlemk8  41208  cdlemk9  41209  cdlemk9bN  41210  cdlemk31  41266  cdlemk32  41267  cdlemk28-3  41278  cdlemk19u  41340  cdlemk56w  41343  tendoex  41345  erngdvlem4  41361  erngdvlem4-rN  41369  dia11N  41418  dib11N  41530  cdlemn6  41572  cdlemn7  41573  cdlemn8  41574  cdlemn9  41575  dihordlem6  41583  dihordlem7  41584  dihord1  41588  dihord2a  41589  dihord2b  41590  dihord2pre  41595  dihord2pre2  41596  dihlsscpre  41604  dihvalcq2  41617  dihopelvalcpre  41618  dihord4  41628  dihord6b  41630  dihmeetlem1N  41660  dihglblem3N  41665  dihmeetlem2N  41669  dihglbcpreN  41670  dihmeetcN  41672  dihmeetbclemN  41674  dihmeetlem4preN  41676  dihjatc1  41681  dihjatc2N  41682  dihjatc3  41683  dihmeetlem9N  41685  dihmeetlem13N  41689  dihmeetlem20N  41696  dih1dimatlem0  41698  mapdpglem24  42074  mapdpglem32  42075  baerlem3lem2  42080  baerlem5alem2  42081  baerlem5blem2  42082  mapdh9aOLDN  42160  hdmap14lem6  42243  nnadddir  42634  sn-addlid  42768  mzpsubst  43099  pellexlem5  43184  pellex  43186  pell14qrexpclnn0  43217  pellfundex  43237  qirropth  43259  monotuz  43292  congtr  43316  congmul  43318  congsub  43321  mzpcong  43323  fzmaxdif  43332  jm2.15nn0  43354  idomsubgmo  43544  iunrelexpmin1  44058  iunrelexpmin2  44062  trclimalb2  44076  mnringmulrcld  44578  fourierdlem42  46501  fourierdlem48  46506  fourierdlem80  46538  smfaddlem1  47115  prmdvdsfmtnof1lem1  47938  uhgrimisgrgric  48285  uspgropssxp  48498  lidldomn1  48585  rngccatidALTV  48626  coe1sclmulval  48739  lincdifsn  48778  seposep  49279  iscnrm3rlem8  49300  iscnrm3llem2  49303