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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp12l  1305  simp22l  1311  simp32l  1317  fsnunf  7216  f1resrcmplf1d  7305  f1oiso2  7386  fpr3g  8334  omeulem2  8622  uniinqs  8849  unxpdomlem3  9280  gruina  10933  dedekind  11503  addlid  11523  subaddmulsub  11809  dmdcan  12057  nnadddir  12424  xaddass  13409  xaddass2  13410  xlt2add  13420  xmulasslem3  13446  xadddi2  13457  xadddi2r  13458  expaddzlem  14278  expaddz  14279  expmulz  14281  expdiv  14286  expmordi  14340  modexp  14412  pfxeq  14876  ccatopth2  14897  swrdco  15019  o1add  15813  o1mul  15814  o1sub  15815  fsumsplitsnun  15953  ntrivcvgmul  16103  prmexpb  16927  pcpremul  17053  pcdiv  17062  pcqmul  17063  pcqdiv  17067  4sqlem12  17166  f1ocpbllem  17728  ercpbl  17753  erlecpbl  17754  latjlej12  18661  latmlem12  18677  latj4  18695  latj4rot  18696  gsumsgrpccat  19068  gsmsymgreqlem2  19678  symgsssg  19714  symgfisg  19715  mndodcong  19789  cmn4  20048  ablsub4  20057  abladdsub4  20058  lsm4  20107  abvdom  21120  abvres  21121  abvtrivd  21122  orngmul  21155  lspsnvs  21425  lspsneu  21434  lspfixed  21439  lspexch  21440  lsmcv  21452  lspsolvlem  21453  ring2idlqus1  21648  coe1sclmulfv  22635  matvscacell  22784  m1detdiag  22945  cramerimplem3  23036  cnprest  23640  hausnei2  23704  isreg2  23728  cmpcld  23753  llyrest  23837  nllyrest  23838  elptr  23925  basqtop  24063  hausflimlem  24331  tmdgsum  24447  utop2nei  24602  trcfilu  24645  ssblps  24774  ssbl  24775  prdsxmslem2  24881  tgqioo  25152  metnrm  25215  bndth  25312  ncvspi  25510  ncvs1  25511  cph2ass  25567  lmmbr2  25613  iscau3  25632  bcthlem5  25682  ovolunlem2  25852  dvres2  26265  dvfsumlem2  26380  plyadd  26569  plymul  26570  coeeu  26577  coemullem  26602  aalioulem4  26695  mulcxp  27046  cxplea  27057  cxple2  27058  cxplt2  27059  cxpcn3lem  27108  angcan  27163  ang180lem5  27174  divsqrtsumlem  27340  logexprlim  27585  dchrvmasumlema  27860  dchrisum0lema  27874  logdivsum  27893  log2sumbnd  27904  abvcxp  27975  padicabv  27990  nolesgn2ores  28062  nosupres  28097  nosupbnd1lem1  28098  nosupbnd1lem2  28099  nosupbnd1lem4  28101  nosupbnd1lem5  28102  nosupbnd1lem6  28103  noinffv  28111  noinfres  28112  noinfbnd1lem1  28113  noinfbnd1lem2  28114  noinfbnd1lem4  28116  noinfbnd1lem6  28118  nosupinfsep  28122  cutbdaylt  28217  expsgt0  28856  bdayfinbndlem1  28886  tghilberti2  29139  brbtwn2  29516  axcontlem4  29578  axcontlem8  29582  clwlkl1loop  30403  clwwlknonex2lem2  30732  umgr2cycllem  30779  clwlknon2num  31002  numclwlk1lem2  31004  chscllem4  32275  measxun2  34926  measun  34927  mbfmco2  34980  probun  35134  satfv1fvfmla1  36368  cgrcomim  36945  cgrcoml  36952  cgrcomr  36953  cgrdegen  36960  btwnintr  36975  btwnexch3  36976  btwnouttr2  36978  btwnouttr  36980  btwnexch  36981  btwndiff  36983  lineid  37039  idinside  37040  btwnconn1lem7  37049  btwnconn1lem8  37050  btwnconn1lem9  37051  btwnconn1lem12  37054  btwnconn1lem14  37056  btwnconn3  37059  midofsegid  37060  segcon2  37061  brsegle2  37065  btwnoutside  37081  outsideoftr  37085  outsideofeu  37087  linethru  37109  cnres2  38900  heibor  38958  lsmsat  40268  lkrlsp  40362  lkrlsp2  40363  lkrlsp3  40364  latm4  40493  omlspjN  40521  hlatj4  40634  4noncolr3  40713  4noncolr2  40714  4noncolr1  40715  athgt  40716  3dimlem3a  40720  3dimlem4a  40723  3dimlem4  40724  3dimlem4OLDN  40725  3dim3  40729  1cvratex  40733  hlatexch4  40741  3atlem4  40746  atcvrlln2  40779  atcvrlln  40780  lplnnlelln  40803  lvoli2  40841  lvolnlelln  40844  lvolnlelpln  40845  4atlem11b  40868  4atlem12b  40871  2lplnja  40879  2lplnj  40880  dalemyeo  40892  dath2  40997  lncvrat  41042  cdlemblem  41053  cdlemb  41054  elpaddri  41062  padd4N  41100  llnmod2i2  41123  llnexchb2  41129  dalawlem1  41131  dalawlem2  41132  pclfinN  41160  osumcllem6N  41221  pexmidlem3N  41232  lhp2lt  41261  lhp2at0  41292  lhp2atnle  41293  lhp2atne  41294  lhp2at0nle  41295  lhp2at0ne  41296  lhpelim  41297  lhpmod2i2  41298  lhpmod6i1  41299  lhple  41302  lhpat  41303  lhpat3  41306  ltrncoelN  41403  ltrncoat  41404  ltrncnv  41406  trlat  41429  trl0  41430  ltrnnidn  41434  trlnid  41439  cdlemd7  41464  cdleme0b  41472  cdleme0c  41473  cdleme0fN  41478  cdleme02N  41482  cdleme0ex1N  41483  cdleme0ex2N  41484  cdleme7aa  41502  cdleme7c  41505  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme8  41510  cdleme11a  41520  cdleme17c  41548  cdleme22gb  41554  cdlemeda  41558  cdleme20k  41579  cdleme21a  41585  cdleme21d  41590  cdleme22f2  41607  cdleme22g  41608  cdleme23a  41609  cdleme23b  41610  cdleme23c  41611  cdleme24  41612  cdleme28  41633  cdlemefrs32fva1  41661  cdlemefr32sn2aw  41664  cdlemefs32sn1aw  41674  cdleme41sn3a  41693  cdleme32fva  41697  cdleme32fva1  41698  cdleme35a  41708  cdleme35b  41710  cdleme35c  41711  cdleme35f  41714  cdleme39a  41725  cdleme42a  41731  cdleme42c  41732  cdleme42b  41738  cdleme42e  41739  cdleme42f  41740  cdleme42g  41741  cdleme42h  41742  cdleme43bN  41750  cdleme46f2g2  41753  cdleme17d2  41755  cdleme17d4  41757  cdleme48fv  41759  cdleme48fvg  41760  cdleme4gfv  41767  cdlemeg46c  41773  cdlemeg46nlpq  41777  cdlemeg46gfre  41792  cdleme48d  41795  cdlemeg49lebilem  41799  cdleme50trn2  41811  cdleme50ltrn  41817  cdleme  41820  cdlemf1  41821  cdlemf  41823  trlord  41829  ltrniotacnvval  41842  ltrniotavalbN  41844  cdlemg1cex  41848  cdlemg2dN  41850  cdlemg2ce  41852  cdlemg2fvlem  41854  cdlemg2idN  41856  cdlemg2kq  41862  cdlemg2l  41863  cdlemg2m  41864  cdlemg4b2  41870  cdlemg7fvN  41884  cdlemg8a  41887  cdlemg10bALTN  41896  cdlemg11aq  41898  cdlemg12d  41906  cdlemg13a  41911  cdlemg13  41912  cdlemg14f  41913  cdlemg14g  41914  cdlemg17a  41921  cdlemg17b  41922  cdlemg27a  41952  cdlemg31b0N  41954  cdlemg31a  41957  cdlemg31b  41958  cdlemg31c  41959  ltrnco  41979  trlcoabs  41981  trlcoabs2N  41982  trlcocnvat  41984  trlconid  41985  trlcolem  41986  trlcone  41988  cdlemg42  41989  cdlemg43  41990  cdlemg46  41995  cdlemg47  41996  tendoeq1  42024  tendoco2  42028  tendoplco2  42039  tendopltp  42040  cdlemh1  42075  cdlemh2  42076  cdlemi1  42078  cdlemi  42080  cdlemk1  42091  cdlemk2  42092  cdlemk3  42093  cdlemk4  42094  cdlemk8  42098  cdlemk9  42099  cdlemk9bN  42100  cdlemk31  42156  cdlemk32  42157  cdlemk28-3  42168  cdlemk19u  42230  cdlemk56w  42233  tendoex  42235  erngdvlem4  42251  erngdvlem4-rN  42259  dia11N  42308  dib11N  42420  cdlemn6  42462  cdlemn7  42463  cdlemn8  42464  cdlemn9  42465  dihordlem6  42473  dihordlem7  42474  dihord1  42478  dihord2a  42479  dihord2b  42480  dihord2pre  42485  dihord2pre2  42486  dihlsscpre  42494  dihvalcq2  42507  dihopelvalcpre  42508  dihord4  42518  dihord6b  42520  dihmeetlem1N  42550  dihglblem3N  42555  dihmeetlem2N  42559  dihglbcpreN  42560  dihmeetcN  42562  dihmeetbclemN  42564  dihmeetlem4preN  42566  dihjatc1  42571  dihjatc2N  42572  dihjatc3  42573  dihmeetlem9N  42575  dihmeetlem13N  42579  dihmeetlem20N  42586  dih1dimatlem0  42588  mapdpglem24  42964  mapdpglem32  42965  baerlem3lem2  42970  baerlem5alem2  42971  baerlem5blem2  42972  mapdh9aOLDN  43050  hdmap14lem6  43133  sn-addlid  43659  mzpsubst  43963  pellexlem5  44044  pellex  44046  pell14qrexpclnn0  44077  pellfundex  44097  qirropth  44119  monotuz  44152  congtr  44176  congmul  44178  congsub  44181  mzpcong  44183  fzmaxdif  44192  jm2.15nn0  44214  idomsubgmo  44398  iunrelexpmin1  44911  iunrelexpmin2  44915  trclimalb2  44929  mnringmulrcld  45429  fourierdlem42  47374  fourierdlem48  47379  fourierdlem80  47411  smfaddlem1  47988  prmdvdsfmtnof1lem1  48884  uhgrimisgrgric  49244  uspgropssxp  49457  lidldomn1  49543  rngccatidALTV  49584  coe1sclmulval  49712  lincdifsn  49751  seposep  50255  iscnrm3rlem8  50276  iscnrm3llem2  50279