Theorem simp3l 1202

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3l	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1135	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:  simp13l  1289  simp23l  1295  simp33l  1301  tfisi  7835  fpr3g  8264  tfrlem5  8348  omeulem1  8546  omeulem2  8547  uniinqs  8770  elfiun  9381  tcrank  9837  isfin2-2  10272  konigthlem  10521  gruen  10765  addlid  11357  mulcan  11815  mulcan2  11816  divass  11855  divdir  11862  div11OLD  11866  muldivdir  11875  subdivcomb1  11877  subdivcomb2  11878  divcan5  11884  ltmul1  12032  ltdiv1  12047  ltmuldiv  12056  lediv2  12073  xaddass2  13210  xlt2add  13220  xmulasslem3  13246  xadddi2  13257  expaddz  14071  expmulz  14073  muldivbinom2  14228  resqrtcl  15219  o1add  15580  o1mul  15581  o1sub  15582  dvdsadd2b  16276  dvdsgcd  16514  rpexp12i  16694  pythagtriplem3  16789  pcpremul  16814  pceu  16817  pcqmul  16824  pcqdiv  16828  setsstruct  17146  f1ocpbllem  17487  funcoppc  17837  funcres  17858  catcisolem  18072  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  latjlej12  18414  latmlem12  18430  latj4  18448  latj4rot  18449  symgsssg  19397  symgfisg  19398  psgnunilem4  19427  odcong  19479  cmn4  19731  ablsub4  19740  abladdsub4  19741  lsm4  19790  abvdom  20739  abvres  20740  abvtrivd  20741  lspsolvlem  21052  lbsextlem2  21069  lidlsubcl  21134  frlmbas3  21685  matmulcell  22332  marrepeval  22450  ma1repveval  22458  submaeval  22469  mdetunilem3  22501  mdetuni0  22508  mdetmul  22510  minmar1eval  22536  nllyrest  23373  hausflimlem  23866  tsmsxp  24042  psmetlecl  24203  xmetlecl  24234  prdsxmetlem  24256  ngpocelbl  24592  bndth  24857  cph2ass  25113  iscau3  25178  dvres2  25813  coemullem  26155  vieta1  26220  aalioulem4  26243  cxpcn3lem  26657  angcan  26712  dchrvmasumlema  27411  logdivsum  27444  abvcxp  27526  padicabv  27541  nosupbnd1lem4  27623  nosupbnd1lem5  27624  noinfbnd1lem4  27638  cofcut1  27828  cofcut2  27830  divsmulw  28096  precsexlem8  28116  precsexlem9  28117  ax5seglem3  28858  ax5seglem6  28861  axpasch  28868  axeuclid  28890  axcontlem4  28894  axcontlem8  28898  wlkl1loop  29566  trlsonwlkon  29638  pthontrlon  29677  wspthsswwlknon  29851  frgr2wwlkeqm  30260  adjlnop  32015  xreceu  32842  orngmul  33281  rhmdvd  33296  measvunilem  34202  measvunilem0  34203  measres  34212  bnj1128  34980  umgr2cycllem  35127  umgr2cycl  35128  satfv1fvfmla1  35410  cgrcomim  35977  cgrcoml  35984  cgrcomr  35985  cgrdegen  35992  segconeu  35999  btwnintr  36007  btwnexch3  36008  btwnouttr2  36010  btwnouttr  36012  btwnexch  36013  trisegint  36016  lineext  36064  linecgr  36069  lineid  36071  idinside  36072  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem7  36081  btwnconn1lem14  36088  btwnconn2  36090  midofsegid  36092  btwnoutside  36113  outsideoftr  36117  lineunray  36135  lineelsb2  36136  cnres2  37757  heibor  37815  lsmcv2  39022  lcvat  39023  lcvexchlem4  39030  lcvexchlem5  39031  lfladd  39059  lflsub  39060  lflmul  39061  lshpkrlem4  39106  latm4  39226  omlmod1i2N  39253  cvlatexch3  39331  cvlsupr7  39341  hlatj4  39367  hlrelat3  39406  cvrval3  39407  atcvrj1  39425  atlelt  39432  2atlt  39433  2atjm  39439  3noncolr2  39443  athgt  39450  3dimlem2  39453  3dimlem4  39458  3dimlem4OLDN  39459  3dim3  39463  1cvratex  39467  ps-1  39471  ps-2  39472  hlatexch3N  39474  llnle  39512  atcvrlln2  39513  atcvrlln  39514  lplni2  39531  lplnle  39534  lplnnle2at  39535  llncvrlpln2  39551  lplnexllnN  39558  2llnmeqat  39565  lvolnle3at  39576  4atlem0ae  39588  lplncvrlvol2  39609  lnjatN  39774  lncvrat  39776  cdlemblem  39787  elpaddri  39796  paddasslem2  39815  paddasslem16  39829  padd4N  39834  hlmod1i  39850  dalawlem2  39866  pclfinN  39894  pexmidlem4N  39967  pl42lem1N  39973  lhp2lt  39995  lhpexle1  40002  lhpexle2lem  40003  lhpj1  40016  lhpmcvr5N  40021  lhp2at0  40026  lhp2atnle  40027  lhp2at0nle  40029  lhple  40036  lhpat  40037  lhpat4N  40038  4atexlempnq  40049  4atexlem7  40069  4atex  40070  ltrn11  40120  ltrnle  40123  ltrnm  40125  ltrnj  40126  ltrncvr  40127  ltrnel  40133  ltrncnvel  40136  ltrncnv  40140  trlval2  40157  trlcnv  40159  trljat1  40160  trljat2  40161  trlat  40163  trl0  40164  trlnidat  40167  trlnid  40173  cdlemc1  40185  cdlemc2  40186  cdlemc5  40189  cdlemd2  40193  cdlemd7  40198  cdlemd8  40199  cdlemd9  40200  cdleme0e  40211  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme5  40234  cdleme10  40248  cdleme11a  40254  cdleme11c  40255  cdleme11h  40260  cdleme11j  40261  cdleme0nex  40284  cdleme18a  40285  cdleme18b  40286  cdleme22gb  40288  cdleme20zN  40295  cdleme20c  40305  cdleme20k  40313  cdleme21a  40319  cdleme21b  40320  cdleme21c  40321  cdleme21h  40328  cdleme22b  40335  cdleme22d  40337  cdleme22f  40340  cdleme25a  40347  cdleme25c  40349  cdleme25dN  40350  cdleme26ee  40354  cdleme30a  40372  cdlemefr29bpre0N  40400  cdlemefr29clN  40401  cdlemefr32fvaN  40403  cdlemefr32fva1  40404  cdlemefs29bpre0N  40410  cdlemefs29bpre1N  40411  cdlemefs29cpre1N  40412  cdlemefs29clN  40413  cdleme43fsv1snlem  40414  cdlemefs32fvaN  40416  cdlemefs32fva1  40417  cdlemefs31fv1  40418  cdleme36a  40454  cdleme39a  40459  cdleme42a  40465  cdleme42c  40466  cdleme17d3  40490  cdleme48fv  40493  cdleme48bw  40496  cdleme48b  40497  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemeg46gfv  40524  cdleme48d  40529  cdleme50trn2a  40544  cdleme50trn2  40545  cdleme50ltrn  40551  cdlemf1  40555  cdlemf  40557  trlord  40563  cdlemg2dN  40584  cdlemg2fvlem  40588  cdlemg2l  40597  cdlemg7fvbwN  40601  cdlemg7aN  40619  cdlemg10bALTN  40630  cdlemg10c  40633  cdlemg17a  40655  cdlemg17dALTN  40658  cdlemg31b0a  40689  cdlemg31a  40691  cdlemg31b  40692  cdlemg34  40706  cdlemg36  40708  ltrnco  40713  trlcoabs2N  40716  trlcolem  40720  cdlemg48  40731  tgrpov  40742  tendoco2  40762  tendoplco2  40773  cdlemh1  40809  cdlemi1  40812  cdlemi2  40813  cdlemj3  40817  tendoid0  40819  cdlemk1  40825  cdlemk2  40826  cdlemk4  40828  cdlemk8  40832  cdlemk9  40833  cdlemk9bN  40834  cdlemk10  40837  cdlemk26b-3  40899  cdlemk26-3  40900  cdlemk28-3  40902  cdlemk37  40908  cdlemk39  40910  cdlemkfid1N  40915  cdlemkid1  40916  cdlemky  40920  cdlemkyu  40921  cdlemk19ylem  40924  cdlemk19xlem  40936  cdlemk11t  40940  cdlemk51  40947  cdlemkyyN  40956  cdleml6  40975  cdleml7  40976  cdleml8  40977  cdleml9  40978  erngdvlem4  40985  erngdvlem4-rN  40993  tendospcanN  41017  dia11N  41042  cdlemm10N  41112  dib11N  41154  dicvaddcl  41184  dicvscacl  41185  cdlemn6  41196  dihvalcq2  41241  dihopelvalcpre  41242  dihord6b  41254  dihord5apre  41256  dihmeetlem1N  41284  dihmeetlem2N  41293  dihglbcpreN  41294  dihjatc1  41305  dihmeetlem20N  41320  dih1dimatlem0  41322  dihatlat  41328  dihglblem6  41334  dochexmidlem4  41457  mapdpglem32  41699  mapdh8ad  41773  mapdh9aOLDN  41784  hdmap11lem2  41836  hdmap14lem6  41867  frlmfzowrdb  42492  flt4lem5  42638  mzpsubst  42736  pellex  42823  pellfundex  42874  pellfund14gap  42875  qirropth  42896  rmxypos  42936  congmul  42956  congsub  42959  mzpcong  42961  coprmdvdsb  42974  jm2.15nn0  42992  jm2.16nn0  42993  rpnnen3lem  43020  idomsubgmo  43182  relexp01min  43702  mullimc  45614  islptre  45617  limccog  45618  mullimcf  45621  addlimc  45646  0ellimcdiv  45647  limsupre3lem  45730  stoweidlem57  46055  fourierdlem48  46152  fourierdlem80  46184  fourierdlem113  46217  ovncvrrp  46562  opnvonmbllem2  46631  ovolval5lem3  46652  ovnovollem3  46656  itsclc0lem1  48745  itsclc0lem2  48746  itschlc0yqe  48749  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  swapffunc  49271  fucofunc  49348  fucoppc  49399