Theorem simp2l 1198

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 1133	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  1285  simp22l  1291  simp32l  1297  fsnunf  7204  f1oiso2  7371  fpr3g  8308  omeulem2  8619  uniinqs  8835  unxpdomlem3  9285  gruina  10855  dedekind  11421  addlid  11441  subaddmulsub  11723  dmdcan  11974  xaddass  13287  xaddass2  13288  xlt2add  13298  xmulasslem3  13324  xadddi2  13335  xadddi2r  13336  expaddzlem  14142  expaddz  14143  expmulz  14145  expdiv  14150  expmordi  14203  modexp  14273  pfxeq  14730  ccatopth2  14751  swrdco  14872  o1add  15646  o1mul  15647  o1sub  15648  fsumsplitsnun  15787  ntrivcvgmul  15934  prmexpb  16752  pcpremul  16876  pcdiv  16885  pcqmul  16886  pcqdiv  16890  4sqlem12  16989  f1ocpbllem  17570  ercpbl  17595  erlecpbl  17596  latjlej12  18512  latmlem12  18528  latj4  18546  latj4rot  18547  gsumsgrpccat  18865  gsmsymgreqlem2  19463  symgsssg  19499  symgfisg  19500  mndodcong  19574  cmn4  19833  ablsub4  19842  abladdsub4  19843  lsm4  19892  abvdom  20847  abvres  20848  abvtrivd  20849  lspsnvs  21133  lspsneu  21142  lspfixed  21147  lspexch  21148  lsmcv  21160  lspsolvlem  21161  ring2idlqus1  21346  coe1sclmulfv  22301  matvscacell  22457  m1detdiag  22618  cramerimplem3  22706  cnprest  23312  hausnei2  23376  isreg2  23400  cmpcld  23425  llyrest  23508  nllyrest  23509  elptr  23596  basqtop  23734  hausflimlem  24002  tmdgsum  24118  utop2nei  24274  trcfilu  24318  ssblps  24447  ssbl  24448  prdsxmslem2  24557  tgqioo  24835  metnrm  24897  bndth  25003  ncvspi  25203  ncvs1  25204  cph2ass  25260  lmmbr2  25306  iscau3  25325  bcthlem5  25375  ovolunlem2  25546  dvres2  25961  dvfsumlem2  26081  dvfsumlem2OLD  26082  plyadd  26270  plymul  26271  coeeu  26278  coemullem  26303  aalioulem4  26391  mulcxp  26741  cxplea  26752  cxple2  26753  cxplt2  26754  cxpcn3lem  26804  angcan  26859  ang180lem5  26870  divsqrtsumlem  27037  logexprlim  27283  dchrvmasumlema  27558  dchrisum0lema  27572  logdivsum  27591  log2sumbnd  27602  abvcxp  27673  padicabv  27688  nolesgn2ores  27731  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem2  27768  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd1lem6  27772  noinffv  27780  noinfres  27781  noinfbnd1lem1  27782  noinfbnd1lem2  27783  noinfbnd1lem4  27785  noinfbnd1lem6  27787  nosupinfsep  27791  scutbdaylt  27877  expsgt0  28429  tghilberti2  28660  brbtwn2  28934  axcontlem4  28996  axcontlem8  29000  clwlkl1loop  29815  clwwlknonex2lem2  30136  clwlknon2num  30396  numclwlk1lem2  30398  chscllem4  31668  orngmul  33312  measxun2  34190  measun  34191  mbfmco2  34246  probun  34400  satfv1fvfmla1  35407  cgrcomim  35970  cgrcoml  35977  cgrcomr  35978  cgrdegen  35985  btwnintr  36000  btwnexch3  36001  btwnouttr2  36003  btwnouttr  36005  btwnexch  36006  btwndiff  36008  lineid  36064  idinside  36065  btwnconn1lem7  36074  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem12  36079  btwnconn1lem14  36081  btwnconn3  36084  midofsegid  36085  segcon2  36086  brsegle2  36090  btwnoutside  36106  outsideoftr  36110  outsideofeu  36112  linethru  36134  cnres2  37749  heibor  37807  lsmsat  38989  lkrlsp  39083  lkrlsp2  39084  lkrlsp3  39085  latm4  39214  omlspjN  39242  hlatj4  39355  4noncolr3  39435  4noncolr2  39436  4noncolr1  39437  athgt  39438  3dimlem3a  39442  3dimlem4a  39445  3dimlem4  39446  3dimlem4OLDN  39447  3dim3  39451  1cvratex  39455  hlatexch4  39463  3atlem4  39468  atcvrlln2  39501  atcvrlln  39502  lplnnlelln  39525  lvoli2  39563  lvolnlelln  39566  lvolnlelpln  39567  4atlem11b  39590  4atlem12b  39593  2lplnja  39601  2lplnj  39602  dalemyeo  39614  dath2  39719  lncvrat  39764  cdlemblem  39775  cdlemb  39776  elpaddri  39784  padd4N  39822  llnmod2i2  39845  llnexchb2  39851  dalawlem1  39853  dalawlem2  39854  pclfinN  39882  osumcllem6N  39943  pexmidlem3N  39954  lhp2lt  39983  lhp2at0  40014  lhp2atnle  40015  lhp2atne  40016  lhp2at0nle  40017  lhp2at0ne  40018  lhpelim  40019  lhpmod2i2  40020  lhpmod6i1  40021  lhple  40024  lhpat  40025  lhpat3  40028  ltrncoelN  40125  ltrncoat  40126  ltrncnv  40128  trlat  40151  trl0  40152  ltrnnidn  40156  trlnid  40161  cdlemd7  40186  cdleme0b  40194  cdleme0c  40195  cdleme0fN  40200  cdleme02N  40204  cdleme0ex1N  40205  cdleme0ex2N  40206  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme8  40232  cdleme11a  40242  cdleme17c  40270  cdleme22gb  40276  cdlemeda  40280  cdleme20k  40301  cdleme21a  40307  cdleme21d  40312  cdleme22f2  40329  cdleme22g  40330  cdleme23a  40331  cdleme23b  40332  cdleme23c  40333  cdleme24  40334  cdleme28  40355  cdlemefrs32fva1  40383  cdlemefr32sn2aw  40386  cdlemefs32sn1aw  40396  cdleme41sn3a  40415  cdleme32fva  40419  cdleme32fva1  40420  cdleme35a  40430  cdleme35b  40432  cdleme35c  40433  cdleme35f  40436  cdleme39a  40447  cdleme42a  40453  cdleme42c  40454  cdleme42b  40460  cdleme42e  40461  cdleme42f  40462  cdleme42g  40463  cdleme42h  40464  cdleme43bN  40472  cdleme46f2g2  40475  cdleme17d2  40477  cdleme17d4  40479  cdleme48fv  40481  cdleme48fvg  40482  cdleme4gfv  40489  cdlemeg46c  40495  cdlemeg46nlpq  40499  cdlemeg46gfre  40514  cdleme48d  40517  cdlemeg49lebilem  40521  cdleme50trn2  40533  cdleme50ltrn  40539  cdleme  40542  cdlemf1  40543  cdlemf  40545  trlord  40551  ltrniotacnvval  40564  ltrniotavalbN  40566  cdlemg1cex  40570  cdlemg2dN  40572  cdlemg2ce  40574  cdlemg2fvlem  40576  cdlemg2idN  40578  cdlemg2kq  40584  cdlemg2l  40585  cdlemg2m  40586  cdlemg4b2  40592  cdlemg7fvN  40606  cdlemg8a  40609  cdlemg10bALTN  40618  cdlemg11aq  40620  cdlemg12d  40628  cdlemg13a  40633  cdlemg13  40634  cdlemg14f  40635  cdlemg14g  40636  cdlemg17a  40643  cdlemg17b  40644  cdlemg27a  40674  cdlemg31b0N  40676  cdlemg31a  40679  cdlemg31b  40680  cdlemg31c  40681  ltrnco  40701  trlcoabs  40703  trlcoabs2N  40704  trlcocnvat  40706  trlconid  40707  trlcolem  40708  trlcone  40710  cdlemg42  40711  cdlemg43  40712  cdlemg46  40717  cdlemg47  40718  tendoeq1  40746  tendoco2  40750  tendoplco2  40761  tendopltp  40762  cdlemh1  40797  cdlemh2  40798  cdlemi1  40800  cdlemi  40802  cdlemk1  40813  cdlemk2  40814  cdlemk3  40815  cdlemk4  40816  cdlemk8  40820  cdlemk9  40821  cdlemk9bN  40822  cdlemk31  40878  cdlemk32  40879  cdlemk28-3  40890  cdlemk19u  40952  cdlemk56w  40955  tendoex  40957  erngdvlem4  40973  erngdvlem4-rN  40981  dia11N  41030  dib11N  41142  cdlemn6  41184  cdlemn7  41185  cdlemn8  41186  cdlemn9  41187  dihordlem6  41195  dihordlem7  41196  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord2pre  41207  dihord2pre2  41208  dihlsscpre  41216  dihvalcq2  41229  dihopelvalcpre  41230  dihord4  41240  dihord6b  41242  dihmeetlem1N  41272  dihglblem3N  41277  dihmeetlem2N  41281  dihglbcpreN  41282  dihmeetcN  41284  dihmeetbclemN  41286  dihmeetlem4preN  41288  dihjatc1  41293  dihjatc2N  41294  dihjatc3  41295  dihmeetlem9N  41297  dihmeetlem13N  41301  dihmeetlem20N  41308  dih1dimatlem0  41310  mapdpglem24  41686  mapdpglem32  41687  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  mapdh9aOLDN  41772  hdmap14lem6  41855  nnadddir  42283  sn-addlid  42410  mzpsubst  42735  pellexlem5  42820  pellex  42822  pell14qrexpclnn0  42853  pellfundex  42873  qirropth  42895  monotuz  42929  congtr  42953  congmul  42955  congsub  42958  mzpcong  42960  fzmaxdif  42969  jm2.15nn0  42991  idomsubgmo  43181  iunrelexpmin1  43697  iunrelexpmin2  43701  trclimalb2  43715  mnringmulrcld  44223  fourierdlem42  46104  fourierdlem48  46109  fourierdlem80  46141  smfaddlem1  46718  prmdvdsfmtnof1lem1  47508  uhgrimisgrgric  47836  uspgropssxp  47987  lidldomn1  48074  rngccatidALTV  48115  coe1sclmulval  48230  lincdifsn  48269  seposep  48721  iscnrm3rlem8  48743  iscnrm3llem2  48746