Theorem simp2l 1080

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl2l  1107  simpr2l  1113  simp12l  1167  simp22l  1173  simp32l  1179  funprgOLD  5855  fsnunf  6356  f1oiso2  6502  omeulem2  7550  uniinqs  7714  unxpdomlem3  8051  gruina  9519  dedekind  10079  addid2  10098  dmdcan  10614  xaddass  11951  xaddass2  11952  xlt2add  11962  xmulasslem3  11988  xadddi2  11999  xadddi2r  12000  expaddzlem  12765  expaddz  12766  expmulz  12768  expdiv  12773  modexp  12861  ccatopth2  13323  swrdco  13434  o1add  14192  o1mul  14193  o1sub  14194  ntrivcvgmul  14473  prmexpb  15268  pcpremul  15386  pcdiv  15395  pcqmul  15396  pcqdiv  15400  4sqlem12  15498  f1ocpbllem  16007  ercpbl  16032  erlecpbl  16033  latjlej12  16890  latmlem12  16906  latj4  16924  latj4rot  16925  symgsssg  17710  symgfisg  17711  mndodcong  17784  cmn4  18035  ablsub4  18041  abladdsub4  18042  lsm4  18086  abvdom  18661  abvres  18662  abvtrivd  18663  lspsnvs  18935  lspsneu  18944  lspfixed  18949  lspexch  18950  lsmcv  18962  lspsolvlem  18963  coe1sclmulfv  19474  matvscacell  20061  m1detdiag  20222  cramerimplem3  20310  cnprest  20903  hausnei2  20967  isreg2  20991  cmpcld  21015  llyrest  21098  nllyrest  21099  elptr  21186  basqtop  21324  hausflimlem  21593  tmdgsum  21709  utop2nei  21864  trcfilu  21908  ssblps  22037  ssbl  22038  prdsxmslem2  22144  tgqioo  22411  metnrm  22473  bndth  22565  ncvspi  22764  ncvs1  22765  cph2ass  22821  lmmbr2  22865  iscau3  22884  bcthlem5  22933  ovolunlem2  23073  dvres2  23482  dvfsumlem2  23594  plyadd  23777  plymul  23778  coeeu  23785  coemullem  23810  aalioulem4  23894  mulcxp  24231  cxplea  24242  cxple2  24243  cxplt2  24244  cxpcn3lem  24288  angcan  24332  ang180lem5  24343  divsqrtsumlem  24506  logexprlim  24750  dchrvmasumlema  24989  dchrisum0lema  25003  logdivsum  25022  log2sumbnd  25033  abvcxp  25104  padicabv  25119  tghilberti2  25333  brbtwn2  25585  axcontlem4  25647  axcontlem8  25651  1pthon  26121  clwwlkel  26321  chscllem4  27883  orngmul  29134  measxun2  29600  measun  29601  mbfmco2  29654  probun  29808  nofulllem5  31105  cgrcomim  31266  cgrcoml  31273  cgrcomr  31274  cgrdegen  31281  btwnintr  31296  btwnexch3  31297  btwnouttr2  31299  btwnouttr  31301  btwnexch  31302  btwndiff  31304  lineid  31360  idinside  31361  btwnconn1lem7  31370  btwnconn1lem8  31371  btwnconn1lem9  31372  btwnconn1lem12  31375  btwnconn1lem14  31377  btwnconn3  31380  midofsegid  31381  segcon2  31382  brsegle2  31386  btwnoutside  31402  outsideoftr  31406  outsideofeu  31408  linethru  31430  cnres2  32732  heibor  32790  lsmsat  33313  lkrlsp  33407  lkrlsp2  33408  lkrlsp3  33409  latm4  33538  omlspjN  33566  hlatj4  33678  4noncolr3  33757  4noncolr2  33758  4noncolr1  33759  athgt  33760  3dimlem3a  33764  3dimlem4a  33767  3dimlem4  33768  3dimlem4OLDN  33769  3dim3  33773  1cvratex  33777  hlatexch4  33785  3atlem4  33790  atcvrlln2  33823  atcvrlln  33824  lplnnlelln  33847  lvoli2  33885  lvolnlelln  33888  lvolnlelpln  33889  4atlem11b  33912  4atlem12b  33915  2lplnja  33923  2lplnj  33924  dalemyeo  33936  dath2  34041  lncvrat  34086  cdlemblem  34097  cdlemb  34098  elpaddri  34106  padd4N  34144  llnmod2i2  34167  llnexchb2  34173  dalawlem1  34175  dalawlem2  34176  pclfinN  34204  osumcllem6N  34265  pexmidlem3N  34276  lhp2lt  34305  lhp2at0  34336  lhp2atnle  34337  lhp2atne  34338  lhp2at0nle  34339  lhp2at0ne  34340  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  lhple  34346  lhpat  34347  lhpat3  34350  ltrncoelN  34447  ltrncoat  34448  ltrncnv  34450  trlat  34474  trl0  34475  ltrnnidn  34479  trlnid  34484  cdlemd7  34509  cdleme0b  34517  cdleme0c  34518  cdleme0fN  34523  cdleme02N  34527  cdleme0ex1N  34528  cdleme0ex2N  34529  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme8  34555  cdleme11a  34565  cdleme17c  34593  cdleme22gb  34599  cdlemeda  34603  cdleme20k  34625  cdleme21a  34631  cdleme21d  34636  cdleme22f2  34653  cdleme22g  34654  cdleme23a  34655  cdleme23b  34656  cdleme23c  34657  cdleme24  34658  cdleme28  34679  cdlemefrs32fva1  34707  cdlemefr32sn2aw  34710  cdlemefs32sn1aw  34720  cdleme41sn3a  34739  cdleme32fva  34743  cdleme32fva1  34744  cdleme35a  34754  cdleme35b  34756  cdleme35c  34757  cdleme35f  34760  cdleme39a  34771  cdleme42a  34777  cdleme42c  34778  cdleme42b  34784  cdleme42e  34785  cdleme42f  34786  cdleme42g  34787  cdleme42h  34788  cdleme43bN  34796  cdleme46f2g2  34799  cdleme17d2  34801  cdleme17d4  34803  cdleme48fv  34805  cdleme48fvg  34806  cdleme4gfv  34813  cdlemeg46c  34819  cdlemeg46nlpq  34823  cdlemeg46gfre  34838  cdleme48d  34841  cdlemeg49lebilem  34845  cdleme50trn2  34857  cdleme50ltrn  34863  cdleme  34866  cdlemf1  34867  cdlemf  34869  trlord  34875  ltrniotacnvval  34888  ltrniotavalbN  34890  cdlemg1cex  34894  cdlemg2dN  34896  cdlemg2ce  34898  cdlemg2fvlem  34900  cdlemg2idN  34902  cdlemg2kq  34908  cdlemg2l  34909  cdlemg2m  34910  cdlemg4b2  34916  cdlemg7fvN  34930  cdlemg8a  34933  cdlemg10bALTN  34942  cdlemg11aq  34944  cdlemg12d  34952  cdlemg13a  34957  cdlemg13  34958  cdlemg14f  34959  cdlemg14g  34960  cdlemg17a  34967  cdlemg17b  34968  cdlemg27a  34998  cdlemg31b0N  35000  cdlemg31a  35003  cdlemg31b  35004  cdlemg31c  35005  ltrnco  35025  trlcoabs  35027  trlcoabs2N  35028  trlcocnvat  35030  trlconid  35031  trlcolem  35032  trlcone  35034  cdlemg42  35035  cdlemg43  35036  cdlemg46  35041  cdlemg47  35042  tendoeq1  35070  tendoco2  35074  tendoplco2  35085  tendopltp  35086  cdlemh1  35121  cdlemh2  35122  cdlemi1  35124  cdlemi  35126  cdlemk1  35137  cdlemk2  35138  cdlemk3  35139  cdlemk4  35140  cdlemk8  35144  cdlemk9  35145  cdlemk9bN  35146  cdlemk31  35202  cdlemk32  35203  cdlemk28-3  35214  cdlemk19u  35276  cdlemk56w  35279  tendoex  35281  erngdvlem4  35297  erngdvlem4-rN  35305  dia11N  35355  dib11N  35467  cdlemn6  35509  cdlemn7  35510  cdlemn8  35511  cdlemn9  35512  dihordlem6  35520  dihordlem7  35521  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord2pre  35532  dihord2pre2  35533  dihlsscpre  35541  dihvalcq2  35554  dihopelvalcpre  35555  dihord4  35565  dihord6b  35567  dihmeetlem1N  35597  dihglblem3N  35602  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetcN  35609  dihmeetbclemN  35611  dihmeetlem4preN  35613  dihjatc1  35618  dihjatc2N  35619  dihjatc3  35620  dihmeetlem9N  35622  dihmeetlem13N  35626  dihmeetlem20N  35633  dih1dimatlem0  35635  mapdpglem24  36011  mapdpglem32  36012  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  mapdh9aOLDN  36098  hdmap14lem6  36183  mzpsubst  36329  pellexlem5  36415  pellex  36417  pell14qrexpclnn0  36448  pellfundex  36468  qirropth  36491  monotuz  36524  expmordi  36530  congtr  36550  congmul  36552  congsub  36555  mzpcong  36557  fzmaxdif  36566  jm2.15nn0  36588  idomsubgmo  36795  iunrelexpmin1  37019  iunrelexpmin2  37023  trclimalb2  37037  fourierdlem42  39042  fourierdlem48  39047  fourierdlem80  39079  smfaddlem1  39649  prmdvdsfmtnof1lem1  40034  clwlkl1loop  40989  clwwlksel  41221  lidldomn1  41711  rngccatidALTV  41781  coe1sclmulval  41967  lincdifsn  42007