Theorem simp3l 1200

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 1134	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  simp13l  1287  simp23l  1293  simp33l  1299  tfisi  7852  fpr3g  8276  tfrlem5  8386  omeulem1  8588  omeulem2  8589  uniinqs  8797  elfiun  9431  tcrank  9885  isfin2-2  10320  konigthlem  10569  gruen  10813  addlid  11404  mulcan  11858  mulcan2  11859  divass  11897  divdir  11904  div11  11907  muldivdir  11914  subdivcomb1  11916  subdivcomb2  11917  divcan5  11923  ltmul1  12071  ltdiv1  12085  ltmuldiv  12094  lediv2  12111  xaddass2  13236  xlt2add  13246  xmulasslem3  13272  xadddi2  13283  expaddz  14079  expmulz  14081  muldivbinom2  14230  resqrtcl  15207  o1add  15565  o1mul  15566  o1sub  15567  dvdsadd2b  16256  dvdsgcd  16493  rpexp12i  16668  pythagtriplem3  16758  pcpremul  16783  pceu  16786  pcqmul  16793  pcqdiv  16797  setsstruct  17116  f1ocpbllem  17477  funcoppc  17832  funcres  17853  catcisolem  18070  1stfcl  18159  2ndfcl  18160  prfcl  18165  evlfcl  18185  curf1cl  18191  curfcl  18195  hofcl  18222  latjlej12  18418  latmlem12  18434  latj4  18452  latj4rot  18453  symgsssg  19383  symgfisg  19384  psgnunilem4  19413  odcong  19465  cmn4  19717  ablsub4  19726  abladdsub4  19727  lsm4  19776  abvdom  20677  abvres  20678  abvtrivd  20679  lspsolvlem  20989  lbsextlem2  21006  lidlsubcl  21077  frlmbas3  21641  matmulcell  22267  marrepeval  22385  ma1repveval  22393  submaeval  22404  mdetunilem3  22436  mdetuni0  22443  mdetmul  22445  minmar1eval  22471  nllyrest  23310  hausflimlem  23803  tsmsxp  23979  psmetlecl  24141  xmetlecl  24172  prdsxmetlem  24194  ngpocelbl  24541  bndth  24804  cph2ass  25061  iscau3  25126  dvres2  25761  coemullem  26102  vieta1  26164  aalioulem4  26187  cxpcn3lem  26596  angcan  26648  dchrvmasumlema  27346  logdivsum  27379  abvcxp  27461  padicabv  27476  nosupbnd1lem4  27557  nosupbnd1lem5  27558  noinfbnd1lem4  27572  cofcut1  27753  cofcut2  27755  divsmulw  28005  precsexlem8  28025  precsexlem9  28026  ax5seglem3  28622  ax5seglem6  28625  axpasch  28632  axeuclid  28654  axcontlem4  28658  axcontlem8  28662  wlkl1loop  29328  trlsonwlkon  29400  pthontrlon  29437  wspthsswwlknon  29608  frgr2wwlkeqm  30017  adjlnop  31772  xreceu  32521  orngmul  32857  rhmdvd  32872  measvunilem  33674  measvunilem0  33675  measres  33684  bnj1128  34465  umgr2cycllem  34595  umgr2cycl  34596  satfv1fvfmla1  34878  cgrcomim  35431  cgrcoml  35438  cgrcomr  35439  cgrdegen  35446  segconeu  35453  btwnintr  35461  btwnexch3  35462  btwnouttr2  35464  btwnouttr  35466  btwnexch  35467  trisegint  35470  lineext  35518  linecgr  35523  lineid  35525  idinside  35526  btwnconn1lem3  35531  btwnconn1lem4  35532  btwnconn1lem7  35535  btwnconn1lem14  35542  btwnconn2  35544  midofsegid  35546  btwnoutside  35567  outsideoftr  35571  lineunray  35589  lineelsb2  35590  cnres2  37095  heibor  37153  lsmcv2  38363  lcvat  38364  lcvexchlem4  38371  lcvexchlem5  38372  lfladd  38400  lflsub  38401  lflmul  38402  lshpkrlem4  38447  latm4  38567  omlmod1i2N  38594  cvlatexch3  38672  cvlsupr7  38682  hlatj4  38708  hlrelat3  38747  cvrval3  38748  atcvrj1  38766  atlelt  38773  2atlt  38774  2atjm  38780  3noncolr2  38784  athgt  38791  3dimlem2  38794  3dimlem4  38799  3dimlem4OLDN  38800  3dim3  38804  1cvratex  38808  ps-1  38812  ps-2  38813  hlatexch3N  38815  llnle  38853  atcvrlln2  38854  atcvrlln  38855  lplni2  38872  lplnle  38875  lplnnle2at  38876  llncvrlpln2  38892  lplnexllnN  38899  2llnmeqat  38906  lvolnle3at  38917  4atlem0ae  38929  lplncvrlvol2  38950  lnjatN  39115  lncvrat  39117  cdlemblem  39128  elpaddri  39137  paddasslem2  39156  paddasslem16  39170  padd4N  39175  hlmod1i  39191  dalawlem2  39207  pclfinN  39235  pexmidlem4N  39308  pl42lem1N  39314  lhp2lt  39336  lhpexle1  39343  lhpexle2lem  39344  lhpj1  39357  lhpmcvr5N  39362  lhp2at0  39367  lhp2atnle  39368  lhp2at0nle  39370  lhple  39377  lhpat  39378  lhpat4N  39379  4atexlempnq  39390  4atexlem7  39410  4atex  39411  ltrn11  39461  ltrnle  39464  ltrnm  39466  ltrnj  39467  ltrncvr  39468  ltrnel  39474  ltrncnvel  39477  ltrncnv  39481  trlval2  39498  trlcnv  39500  trljat1  39501  trljat2  39502  trlat  39504  trl0  39505  trlnidat  39508  trlnid  39514  cdlemc1  39526  cdlemc2  39527  cdlemc5  39530  cdlemd2  39534  cdlemd7  39539  cdlemd8  39540  cdlemd9  39541  cdleme0e  39552  cdleme3g  39569  cdleme3h  39570  cdleme3  39572  cdleme5  39575  cdleme10  39589  cdleme11a  39595  cdleme11c  39596  cdleme11h  39601  cdleme11j  39602  cdleme0nex  39625  cdleme18a  39626  cdleme18b  39627  cdleme22gb  39629  cdleme20zN  39636  cdleme20c  39646  cdleme20k  39654  cdleme21a  39660  cdleme21b  39661  cdleme21c  39662  cdleme21h  39669  cdleme22b  39676  cdleme22d  39678  cdleme22f  39681  cdleme25a  39688  cdleme25c  39690  cdleme25dN  39691  cdleme26ee  39695  cdleme30a  39713  cdlemefr29bpre0N  39741  cdlemefr29clN  39742  cdlemefr32fvaN  39744  cdlemefr32fva1  39745  cdlemefs29bpre0N  39751  cdlemefs29bpre1N  39752  cdlemefs29cpre1N  39753  cdlemefs29clN  39754  cdleme43fsv1snlem  39755  cdlemefs32fvaN  39757  cdlemefs32fva1  39758  cdlemefs31fv1  39759  cdleme36a  39795  cdleme39a  39800  cdleme42a  39806  cdleme42c  39807  cdleme17d3  39831  cdleme48fv  39834  cdleme48bw  39837  cdleme48b  39838  cdlemeg46rgv  39863  cdlemeg46req  39864  cdlemeg46gfv  39865  cdleme48d  39870  cdleme50trn2a  39885  cdleme50trn2  39886  cdleme50ltrn  39892  cdlemf1  39896  cdlemf  39898  trlord  39904  cdlemg2dN  39925  cdlemg2fvlem  39929  cdlemg2l  39938  cdlemg7fvbwN  39942  cdlemg7aN  39960  cdlemg10bALTN  39971  cdlemg10c  39974  cdlemg17a  39996  cdlemg17dALTN  39999  cdlemg31b0a  40030  cdlemg31a  40032  cdlemg31b  40033  cdlemg34  40047  cdlemg36  40049  ltrnco  40054  trlcoabs2N  40057  trlcolem  40061  cdlemg48  40072  tgrpov  40083  tendoco2  40103  tendoplco2  40114  cdlemh1  40150  cdlemi1  40153  cdlemi2  40154  cdlemj3  40158  tendoid0  40160  cdlemk1  40166  cdlemk2  40167  cdlemk4  40169  cdlemk8  40173  cdlemk9  40174  cdlemk9bN  40175  cdlemk10  40178  cdlemk26b-3  40240  cdlemk26-3  40241  cdlemk28-3  40243  cdlemk37  40249  cdlemk39  40251  cdlemkfid1N  40256  cdlemkid1  40257  cdlemky  40261  cdlemkyu  40262  cdlemk19ylem  40265  cdlemk19xlem  40277  cdlemk11t  40281  cdlemk51  40288  cdlemkyyN  40297  cdleml6  40316  cdleml7  40317  cdleml8  40318  cdleml9  40319  erngdvlem4  40326  erngdvlem4-rN  40334  tendospcanN  40358  dia11N  40383  cdlemm10N  40453  dib11N  40495  dicvaddcl  40525  dicvscacl  40526  cdlemn6  40537  dihvalcq2  40582  dihopelvalcpre  40583  dihord6b  40595  dihord5apre  40597  dihmeetlem1N  40625  dihmeetlem2N  40634  dihglbcpreN  40635  dihjatc1  40646  dihmeetlem20N  40661  dih1dimatlem0  40663  dihatlat  40669  dihglblem6  40675  dochexmidlem4  40798  mapdpglem32  41040  mapdh8ad  41114  mapdh9aOLDN  41125  hdmap11lem2  41177  hdmap14lem6  41208  frlmfzowrdb  41545  flt4lem5  41855  mzpsubst  41949  pellex  42036  pellfundex  42087  pellfund14gap  42088  qirropth  42109  rmxypos  42149  congmul  42169  congsub  42172  mzpcong  42174  coprmdvdsb  42187  jm2.15nn0  42205  jm2.16nn0  42206  rpnnen3lem  42233  idomsubgmo  42403  relexp01min  42927  mullimc  44791  islptre  44794  limccog  44795  mullimcf  44798  addlimc  44823  0ellimcdiv  44824  limsupre3lem  44907  stoweidlem57  45232  fourierdlem48  45329  fourierdlem80  45361  fourierdlem113  45394  ovncvrrp  45739  opnvonmbllem2  45808  ovolval5lem3  45829  ovnovollem3  45833  itsclc0lem1  47604  itsclc0lem2  47605  itschlc0yqe  47608  itscnhlc0xyqsol  47613  itschlc0xyqsol1  47614