Theorem simp2l 1212

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp12l  1299  simp22l  1305  simp32l  1311  fsnunf  7165  f1oiso2  7332  fpr3g  8261  omeulem2  8547  uniinqs  8774  unxpdomlem3  9198  gruina  10773  dedekind  11343  addlid  11363  subaddmulsub  11647  dmdcan  11898  nnadddir  12266  xaddass  13249  xaddass2  13250  xlt2add  13260  xmulasslem3  13286  xadddi2  13297  xadddi2r  13298  expaddzlem  14115  expaddz  14116  expmulz  14118  expdiv  14123  expmordi  14177  modexp  14248  pfxeq  14706  ccatopth2  14727  swrdco  14847  o1add  15624  o1mul  15625  o1sub  15626  fsumsplitsnun  15765  ntrivcvgmul  15915  prmexpb  16737  pcpremul  16862  pcdiv  16871  pcqmul  16872  pcqdiv  16876  4sqlem12  16975  f1ocpbllem  17537  ercpbl  17562  erlecpbl  17563  latjlej12  18470  latmlem12  18486  latj4  18504  latj4rot  18505  gsumsgrpccat  18857  gsmsymgreqlem2  19454  symgsssg  19490  symgfisg  19491  mndodcong  19565  cmn4  19824  ablsub4  19833  abladdsub4  19834  lsm4  19883  abvdom  20859  abvres  20860  abvtrivd  20861  orngmul  20894  lspsnvs  21164  lspsneu  21173  lspfixed  21178  lspexch  21179  lsmcv  21191  lspsolvlem  21192  ring2idlqus1  21369  coe1sclmulfv  22326  matvscacell  22476  m1detdiag  22637  cramerimplem3  22725  cnprest  23329  hausnei2  23393  isreg2  23417  cmpcld  23442  llyrest  23525  nllyrest  23526  elptr  23613  basqtop  23751  hausflimlem  24019  tmdgsum  24135  utop2nei  24290  trcfilu  24333  ssblps  24462  ssbl  24463  prdsxmslem2  24569  tgqioo  24840  metnrm  24903  bndth  25000  ncvspi  25198  ncvs1  25199  cph2ass  25255  lmmbr2  25301  iscau3  25320  bcthlem5  25370  ovolunlem2  25540  dvres2  25954  dvfsumlem2  26069  plyadd  26257  plymul  26258  coeeu  26265  coemullem  26290  aalioulem4  26376  mulcxp  26727  cxplea  26738  cxple2  26739  cxplt2  26740  cxpcn3lem  26789  angcan  26844  ang180lem5  26855  divsqrtsumlem  27021  logexprlim  27266  dchrvmasumlema  27541  dchrisum0lema  27555  logdivsum  27574  log2sumbnd  27585  abvcxp  27656  padicabv  27671  nolesgn2ores  27713  nosupres  27748  nosupbnd1lem1  27749  nosupbnd1lem2  27750  nosupbnd1lem4  27752  nosupbnd1lem5  27753  nosupbnd1lem6  27754  noinffv  27762  noinfres  27763  noinfbnd1lem1  27764  noinfbnd1lem2  27765  noinfbnd1lem4  27767  noinfbnd1lem6  27769  nosupinfsep  27773  cutbdaylt  27868  expsgt0  28507  bdayfinbndlem1  28537  tghilberti2  28784  brbtwn2  29052  axcontlem4  29114  axcontlem8  29118  clwlkl1loop  29929  clwwlknonex2lem2  30256  clwlknon2num  30516  numclwlk1lem2  30518  chscllem4  31789  measxun2  34468  measun  34469  mbfmco2  34523  probun  34677  satfv1fvfmla1  35737  cgrcomim  36303  cgrcoml  36310  cgrcomr  36311  cgrdegen  36318  btwnintr  36333  btwnexch3  36334  btwnouttr2  36336  btwnouttr  36338  btwnexch  36339  btwndiff  36341  lineid  36397  idinside  36398  btwnconn1lem7  36407  btwnconn1lem8  36408  btwnconn1lem9  36409  btwnconn1lem12  36412  btwnconn1lem14  36414  btwnconn3  36417  midofsegid  36418  segcon2  36419  brsegle2  36423  btwnoutside  36439  outsideoftr  36443  outsideofeu  36445  linethru  36467  cnres2  38226  heibor  38284  lsmsat  39596  lkrlsp  39690  lkrlsp2  39691  lkrlsp3  39692  latm4  39821  omlspjN  39849  hlatj4  39962  4noncolr3  40041  4noncolr2  40042  4noncolr1  40043  athgt  40044  3dimlem3a  40048  3dimlem4a  40051  3dimlem4  40052  3dimlem4OLDN  40053  3dim3  40057  1cvratex  40061  hlatexch4  40069  3atlem4  40074  atcvrlln2  40107  atcvrlln  40108  lplnnlelln  40131  lvoli2  40169  lvolnlelln  40172  lvolnlelpln  40173  4atlem11b  40196  4atlem12b  40199  2lplnja  40207  2lplnj  40208  dalemyeo  40220  dath2  40325  lncvrat  40370  cdlemblem  40381  cdlemb  40382  elpaddri  40390  padd4N  40428  llnmod2i2  40451  llnexchb2  40457  dalawlem1  40459  dalawlem2  40460  pclfinN  40488  osumcllem6N  40549  pexmidlem3N  40560  lhp2lt  40589  lhp2at0  40620  lhp2atnle  40621  lhp2atne  40622  lhp2at0nle  40623  lhp2at0ne  40624  lhpelim  40625  lhpmod2i2  40626  lhpmod6i1  40627  lhple  40630  lhpat  40631  lhpat3  40634  ltrncoelN  40731  ltrncoat  40732  ltrncnv  40734  trlat  40757  trl0  40758  ltrnnidn  40762  trlnid  40767  cdlemd7  40792  cdleme0b  40800  cdleme0c  40801  cdleme0fN  40806  cdleme02N  40810  cdleme0ex1N  40811  cdleme0ex2N  40812  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme8  40838  cdleme11a  40848  cdleme17c  40876  cdleme22gb  40882  cdlemeda  40886  cdleme20k  40907  cdleme21a  40913  cdleme21d  40918  cdleme22f2  40935  cdleme22g  40936  cdleme23a  40937  cdleme23b  40938  cdleme23c  40939  cdleme24  40940  cdleme28  40961  cdlemefrs32fva1  40989  cdlemefr32sn2aw  40992  cdlemefs32sn1aw  41002  cdleme41sn3a  41021  cdleme32fva  41025  cdleme32fva1  41026  cdleme35a  41036  cdleme35b  41038  cdleme35c  41039  cdleme35f  41042  cdleme39a  41053  cdleme42a  41059  cdleme42c  41060  cdleme42b  41066  cdleme42e  41067  cdleme42f  41068  cdleme42g  41069  cdleme42h  41070  cdleme43bN  41078  cdleme46f2g2  41081  cdleme17d2  41083  cdleme17d4  41085  cdleme48fv  41087  cdleme48fvg  41088  cdleme4gfv  41095  cdlemeg46c  41101  cdlemeg46nlpq  41105  cdlemeg46gfre  41120  cdleme48d  41123  cdlemeg49lebilem  41127  cdleme50trn2  41139  cdleme50ltrn  41145  cdleme  41148  cdlemf1  41149  cdlemf  41151  trlord  41157  ltrniotacnvval  41170  ltrniotavalbN  41172  cdlemg1cex  41176  cdlemg2dN  41178  cdlemg2ce  41180  cdlemg2fvlem  41182  cdlemg2idN  41184  cdlemg2kq  41190  cdlemg2l  41191  cdlemg2m  41192  cdlemg4b2  41198  cdlemg7fvN  41212  cdlemg8a  41215  cdlemg10bALTN  41224  cdlemg11aq  41226  cdlemg12d  41234  cdlemg13a  41239  cdlemg13  41240  cdlemg14f  41241  cdlemg14g  41242  cdlemg17a  41249  cdlemg17b  41250  cdlemg27a  41280  cdlemg31b0N  41282  cdlemg31a  41285  cdlemg31b  41286  cdlemg31c  41287  ltrnco  41307  trlcoabs  41309  trlcoabs2N  41310  trlcocnvat  41312  trlconid  41313  trlcolem  41314  trlcone  41316  cdlemg42  41317  cdlemg43  41318  cdlemg46  41323  cdlemg47  41324  tendoeq1  41352  tendoco2  41356  tendoplco2  41367  tendopltp  41368  cdlemh1  41403  cdlemh2  41404  cdlemi1  41406  cdlemi  41408  cdlemk1  41419  cdlemk2  41420  cdlemk3  41421  cdlemk4  41422  cdlemk8  41426  cdlemk9  41427  cdlemk9bN  41428  cdlemk31  41484  cdlemk32  41485  cdlemk28-3  41496  cdlemk19u  41558  cdlemk56w  41561  tendoex  41563  erngdvlem4  41579  erngdvlem4-rN  41587  dia11N  41636  dib11N  41748  cdlemn6  41790  cdlemn7  41791  cdlemn8  41792  cdlemn9  41793  dihordlem6  41801  dihordlem7  41802  dihord1  41806  dihord2a  41807  dihord2b  41808  dihord2pre  41813  dihord2pre2  41814  dihlsscpre  41822  dihvalcq2  41835  dihopelvalcpre  41836  dihord4  41846  dihord6b  41848  dihmeetlem1N  41878  dihglblem3N  41883  dihmeetlem2N  41887  dihglbcpreN  41888  dihmeetcN  41890  dihmeetbclemN  41892  dihmeetlem4preN  41894  dihjatc1  41899  dihjatc2N  41900  dihjatc3  41901  dihmeetlem9N  41903  dihmeetlem13N  41907  dihmeetlem20N  41914  dih1dimatlem0  41916  mapdpglem24  42292  mapdpglem32  42293  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  mapdh9aOLDN  42378  hdmap14lem6  42461  sn-addlid  42977  mzpsubst  43293  pellexlem5  43374  pellex  43376  pell14qrexpclnn0  43407  pellfundex  43427  qirropth  43449  monotuz  43482  congtr  43506  congmul  43508  congsub  43511  mzpcong  43513  fzmaxdif  43522  jm2.15nn0  43544  idomsubgmo  43734  iunrelexpmin1  44248  iunrelexpmin2  44252  trclimalb2  44266  mnringmulrcld  44768  fourierdlem42  46687  fourierdlem48  46692  fourierdlem80  46724  smfaddlem1  47301  prmdvdsfmtnof1lem1  48157  uhgrimisgrgric  48517  uspgropssxp  48730  lidldomn1  48817  rngccatidALTV  48858  coe1sclmulval  48971  lincdifsn  49010  seposep  49511  iscnrm3rlem8  49532  iscnrm3llem2  49535