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 484	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1136	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp13l  1289  simp23l  1295  simp33l  1301  tfisi  7845  fpr3g  8267  tfrlem5  8377  omeulem1  8579  omeulem2  8580  uniinqs  8788  elfiun  9422  tcrank  9876  isfin2-2  10311  konigthlem  10560  gruen  10804  addlid  11394  mulcan  11848  mulcan2  11849  divass  11887  divdir  11894  div11  11897  muldivdir  11904  subdivcomb1  11906  subdivcomb2  11907  divcan5  11913  ltmul1  12061  ltdiv1  12075  ltmuldiv  12084  lediv2  12101  xaddass2  13226  xlt2add  13236  xmulasslem3  13262  xadddi2  13273  expaddz  14069  expmulz  14071  muldivbinom2  14220  resqrtcl  15197  o1add  15555  o1mul  15556  o1sub  15557  dvdsadd2b  16246  dvdsgcd  16483  rpexp12i  16658  pythagtriplem3  16748  pcpremul  16773  pceu  16776  pcqmul  16783  pcqdiv  16787  setsstruct  17106  f1ocpbllem  17467  funcoppc  17822  funcres  17843  catcisolem  18057  1stfcl  18146  2ndfcl  18147  prfcl  18152  evlfcl  18172  curf1cl  18178  curfcl  18182  hofcl  18209  latjlej12  18405  latmlem12  18421  latj4  18439  latj4rot  18440  symgsssg  19330  symgfisg  19331  psgnunilem4  19360  odcong  19412  cmn4  19664  ablsub4  19673  abladdsub4  19674  lsm4  19723  abvdom  20439  abvres  20440  abvtrivd  20441  lspsolvlem  20748  lbsextlem2  20765  lidlsubcl  20832  frlmbas3  21323  matmulcell  21939  marrepeval  22057  ma1repveval  22065  submaeval  22076  mdetunilem3  22108  mdetuni0  22115  mdetmul  22117  minmar1eval  22143  nllyrest  22982  hausflimlem  23475  tsmsxp  23651  psmetlecl  23813  xmetlecl  23844  prdsxmetlem  23866  ngpocelbl  24213  bndth  24466  cph2ass  24722  iscau3  24787  dvres2  25421  coemullem  25756  vieta1  25817  aalioulem4  25840  cxpcn3lem  26245  angcan  26297  dchrvmasumlema  26993  logdivsum  27026  abvcxp  27108  padicabv  27123  nosupbnd1lem4  27204  nosupbnd1lem5  27205  noinfbnd1lem4  27219  cofcut1  27397  cofcut2  27399  divsmulw  27630  precsexlem8  27650  precsexlem9  27651  ax5seglem3  28179  ax5seglem6  28182  axpasch  28189  axeuclid  28211  axcontlem4  28215  axcontlem8  28219  wlkl1loop  28885  trlsonwlkon  28957  pthontrlon  28994  wspthsswwlknon  29165  frgr2wwlkeqm  29574  adjlnop  31327  xreceu  32076  orngmul  32410  rhmdvd  32425  measvunilem  33199  measvunilem0  33200  measres  33209  bnj1128  33990  umgr2cycllem  34120  umgr2cycl  34121  satfv1fvfmla1  34403  cgrcomim  34950  cgrcoml  34957  cgrcomr  34958  cgrdegen  34965  segconeu  34972  btwnintr  34980  btwnexch3  34981  btwnouttr2  34983  btwnouttr  34985  btwnexch  34986  trisegint  34989  lineext  35037  linecgr  35042  lineid  35044  idinside  35045  btwnconn1lem3  35050  btwnconn1lem4  35051  btwnconn1lem7  35054  btwnconn1lem14  35061  btwnconn2  35063  midofsegid  35065  btwnoutside  35086  outsideoftr  35090  lineunray  35108  lineelsb2  35109  cnres2  36620  heibor  36678  lsmcv2  37888  lcvat  37889  lcvexchlem4  37896  lcvexchlem5  37897  lfladd  37925  lflsub  37926  lflmul  37927  lshpkrlem4  37972  latm4  38092  omlmod1i2N  38119  cvlatexch3  38197  cvlsupr7  38207  hlatj4  38233  hlrelat3  38272  cvrval3  38273  atcvrj1  38291  atlelt  38298  2atlt  38299  2atjm  38305  3noncolr2  38309  athgt  38316  3dimlem2  38319  3dimlem4  38324  3dimlem4OLDN  38325  3dim3  38329  1cvratex  38333  ps-1  38337  ps-2  38338  hlatexch3N  38340  llnle  38378  atcvrlln2  38379  atcvrlln  38380  lplni2  38397  lplnle  38400  lplnnle2at  38401  llncvrlpln2  38417  lplnexllnN  38424  2llnmeqat  38431  lvolnle3at  38442  4atlem0ae  38454  lplncvrlvol2  38475  lnjatN  38640  lncvrat  38642  cdlemblem  38653  elpaddri  38662  paddasslem2  38681  paddasslem16  38695  padd4N  38700  hlmod1i  38716  dalawlem2  38732  pclfinN  38760  pexmidlem4N  38833  pl42lem1N  38839  lhp2lt  38861  lhpexle1  38868  lhpexle2lem  38869  lhpj1  38882  lhpmcvr5N  38887  lhp2at0  38892  lhp2atnle  38893  lhp2at0nle  38895  lhple  38902  lhpat  38903  lhpat4N  38904  4atexlempnq  38915  4atexlem7  38935  4atex  38936  ltrn11  38986  ltrnle  38989  ltrnm  38991  ltrnj  38992  ltrncvr  38993  ltrnel  38999  ltrncnvel  39002  ltrncnv  39006  trlval2  39023  trlcnv  39025  trljat1  39026  trljat2  39027  trlat  39029  trl0  39030  trlnidat  39033  trlnid  39039  cdlemc1  39051  cdlemc2  39052  cdlemc5  39055  cdlemd2  39059  cdlemd7  39064  cdlemd8  39065  cdlemd9  39066  cdleme0e  39077  cdleme3g  39094  cdleme3h  39095  cdleme3  39097  cdleme5  39100  cdleme10  39114  cdleme11a  39120  cdleme11c  39121  cdleme11h  39126  cdleme11j  39127  cdleme0nex  39150  cdleme18a  39151  cdleme18b  39152  cdleme22gb  39154  cdleme20zN  39161  cdleme20c  39171  cdleme20k  39179  cdleme21a  39185  cdleme21b  39186  cdleme21c  39187  cdleme21h  39194  cdleme22b  39201  cdleme22d  39203  cdleme22f  39206  cdleme25a  39213  cdleme25c  39215  cdleme25dN  39216  cdleme26ee  39220  cdleme30a  39238  cdlemefr29bpre0N  39266  cdlemefr29clN  39267  cdlemefr32fvaN  39269  cdlemefr32fva1  39270  cdlemefs29bpre0N  39276  cdlemefs29bpre1N  39277  cdlemefs29cpre1N  39278  cdlemefs29clN  39279  cdleme43fsv1snlem  39280  cdlemefs32fvaN  39282  cdlemefs32fva1  39283  cdlemefs31fv1  39284  cdleme36a  39320  cdleme39a  39325  cdleme42a  39331  cdleme42c  39332  cdleme17d3  39356  cdleme48fv  39359  cdleme48bw  39362  cdleme48b  39363  cdlemeg46rgv  39388  cdlemeg46req  39389  cdlemeg46gfv  39390  cdleme48d  39395  cdleme50trn2a  39410  cdleme50trn2  39411  cdleme50ltrn  39417  cdlemf1  39421  cdlemf  39423  trlord  39429  cdlemg2dN  39450  cdlemg2fvlem  39454  cdlemg2l  39463  cdlemg7fvbwN  39467  cdlemg7aN  39485  cdlemg10bALTN  39496  cdlemg10c  39499  cdlemg17a  39521  cdlemg17dALTN  39524  cdlemg31b0a  39555  cdlemg31a  39557  cdlemg31b  39558  cdlemg34  39572  cdlemg36  39574  ltrnco  39579  trlcoabs2N  39582  trlcolem  39586  cdlemg48  39597  tgrpov  39608  tendoco2  39628  tendoplco2  39639  cdlemh1  39675  cdlemi1  39678  cdlemi2  39679  cdlemj3  39683  tendoid0  39685  cdlemk1  39691  cdlemk2  39692  cdlemk4  39694  cdlemk8  39698  cdlemk9  39699  cdlemk9bN  39700  cdlemk10  39703  cdlemk26b-3  39765  cdlemk26-3  39766  cdlemk28-3  39768  cdlemk37  39774  cdlemk39  39776  cdlemkfid1N  39781  cdlemkid1  39782  cdlemky  39786  cdlemkyu  39787  cdlemk19ylem  39790  cdlemk19xlem  39802  cdlemk11t  39806  cdlemk51  39813  cdlemkyyN  39822  cdleml6  39841  cdleml7  39842  cdleml8  39843  cdleml9  39844  erngdvlem4  39851  erngdvlem4-rN  39859  tendospcanN  39883  dia11N  39908  cdlemm10N  39978  dib11N  40020  dicvaddcl  40050  dicvscacl  40051  cdlemn6  40062  dihvalcq2  40107  dihopelvalcpre  40108  dihord6b  40120  dihord5apre  40122  dihmeetlem1N  40150  dihmeetlem2N  40159  dihglbcpreN  40160  dihjatc1  40171  dihmeetlem20N  40186  dih1dimatlem0  40188  dihatlat  40194  dihglblem6  40200  dochexmidlem4  40323  mapdpglem32  40565  mapdh8ad  40639  mapdh9aOLDN  40650  hdmap11lem2  40702  hdmap14lem6  40733  frlmfzowrdb  41076  flt4lem5  41389  mzpsubst  41472  pellex  41559  pellfundex  41610  pellfund14gap  41611  qirropth  41632  rmxypos  41672  congmul  41692  congsub  41695  mzpcong  41697  coprmdvdsb  41710  jm2.15nn0  41728  jm2.16nn0  41729  rpnnen3lem  41756  idomsubgmo  41926  relexp01min  42450  mullimc  44319  islptre  44322  limccog  44323  mullimcf  44326  addlimc  44351  0ellimcdiv  44352  limsupre3lem  44435  stoweidlem57  44760  fourierdlem48  44857  fourierdlem80  44889  fourierdlem113  44922  ovncvrrp  45267  opnvonmbllem2  45336  ovolval5lem3  45357  ovnovollem3  45361  itsclc0lem1  47396  itsclc0lem2  47397  itschlc0yqe  47400  itscnhlc0xyqsol  47405  itschlc0xyqsol1  47406