Theorem simp3l 1181

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simp13l  1268  simp23l  1274  simp33l  1280  tfisi  7391  tfrlem5  7822  omeulem1  8011  omeulem2  8012  uniinqs  8179  elfiun  8691  tcrank  9109  isfin2-2  9541  konigthlem  9790  gruen  10034  addid2  10625  mulcan  11080  mulcan2  11081  divass  11119  divdir  11126  div11  11129  muldivdir  11136  subdivcomb1  11138  subdivcomb2  11139  divcan5  11145  ltmul1  11293  ltdiv1  11307  ltmuldiv  11316  lediv2  11333  xaddass2  12462  xlt2add  12472  xmulasslem3  12498  xadddi2  12509  expaddz  13291  expmulz  13293  muldivbinom2  13441  resqrtcl  14477  o1add  14834  o1mul  14835  o1sub  14836  dvdsadd2b  15519  dvdsgcd  15751  rpexp12i  15925  pythagtriplem3  16014  pcpremul  16039  pceu  16042  pcqmul  16049  pcqdiv  16053  setsstruct  16382  f1ocpbllem  16656  funcoppc  17006  funcres  17027  catcisolem  17227  1stfcl  17308  2ndfcl  17309  prfcl  17314  evlfcl  17333  curf1cl  17339  curfcl  17343  hofcl  17370  latjlej12  17538  latmlem12  17554  latj4  17572  latj4rot  17573  symgsssg  18359  symgfisg  18360  psgnunilem4  18390  odcong  18442  cmn4  18688  ablsub4  18694  abladdsub4  18695  lsm4  18739  abvdom  19334  abvres  19335  abvtrivd  19336  lspsolvlem  19639  lbsextlem2  19656  lidlsubcl  19713  frlmbas3  20625  matmulcell  20761  marrepeval  20879  ma1repveval  20887  submaeval  20898  mdetunilem3  20930  mdetuni0  20937  mdetmul  20939  minmar1eval  20965  nllyrest  21801  hausflimlem  22294  tsmsxp  22469  psmetlecl  22631  xmetlecl  22662  prdsxmetlem  22684  ngpocelbl  23019  bndth  23268  cph2ass  23523  iscau3  23587  dvres2  24216  coemullem  24546  vieta1  24607  aalioulem4  24630  cxpcn3lem  25032  angcan  25084  dchrvmasumlema  25781  logdivsum  25814  abvcxp  25896  padicabv  25911  ax5seglem3  26423  ax5seglem6  26426  axpasch  26433  axeuclid  26455  axcontlem4  26459  axcontlem8  26463  wlkl1loop  27125  trlsonwlkon  27202  pthontrlon  27239  wspthsswwlknon  27430  frgr2wwlkeqm  27868  adjlnop  29647  xreceu  30347  orngmul  30555  rhmdvd  30573  measvunilem  31116  measvunilem0  31117  measres  31126  bnj1128  31907  fpr3g  32643  nosupbnd1lem4  32732  nosupbnd1lem5  32733  cgrcomim  32971  cgrcoml  32978  cgrcomr  32979  cgrdegen  32986  segconeu  32993  btwnintr  33001  btwnexch3  33002  btwnouttr2  33004  btwnouttr  33006  btwnexch  33007  trisegint  33010  lineext  33058  linecgr  33063  lineid  33065  idinside  33066  btwnconn1lem3  33071  btwnconn1lem4  33072  btwnconn1lem7  33075  btwnconn1lem14  33082  btwnconn2  33084  midofsegid  33086  btwnoutside  33107  outsideoftr  33111  lineunray  33129  lineelsb2  33130  cnres2  34483  heibor  34541  lsmcv2  35610  lcvat  35611  lcvexchlem4  35618  lcvexchlem5  35619  lfladd  35647  lflsub  35648  lflmul  35649  lshpkrlem4  35694  latm4  35814  omlmod1i2N  35841  cvlatexch3  35919  cvlsupr7  35929  hlatj4  35955  hlrelat3  35993  cvrval3  35994  atcvrj1  36012  atlelt  36019  2atlt  36020  2atjm  36026  3noncolr2  36030  athgt  36037  3dimlem2  36040  3dimlem4  36045  3dimlem4OLDN  36046  3dim3  36050  1cvratex  36054  ps-1  36058  ps-2  36059  hlatexch3N  36061  llnle  36099  atcvrlln2  36100  atcvrlln  36101  lplni2  36118  lplnle  36121  lplnnle2at  36122  llncvrlpln2  36138  lplnexllnN  36145  2llnmeqat  36152  lvolnle3at  36163  4atlem0ae  36175  lplncvrlvol2  36196  lnjatN  36361  lncvrat  36363  cdlemblem  36374  elpaddri  36383  paddasslem2  36402  paddasslem16  36416  padd4N  36421  hlmod1i  36437  dalawlem2  36453  pclfinN  36481  pexmidlem4N  36554  pl42lem1N  36560  lhp2lt  36582  lhpexle1  36589  lhpexle2lem  36590  lhpj1  36603  lhpmcvr5N  36608  lhp2at0  36613  lhp2atnle  36614  lhp2at0nle  36616  lhple  36623  lhpat  36624  lhpat4N  36625  4atexlempnq  36636  4atexlem7  36656  4atex  36657  ltrn11  36707  ltrnle  36710  ltrnm  36712  ltrnj  36713  ltrncvr  36714  ltrnel  36720  ltrncnvel  36723  ltrncnv  36727  trlval2  36744  trlcnv  36746  trljat1  36747  trljat2  36748  trlat  36750  trl0  36751  trlnidat  36754  trlnid  36760  cdlemc1  36772  cdlemc2  36773  cdlemc5  36776  cdlemd2  36780  cdlemd7  36785  cdlemd8  36786  cdlemd9  36787  cdleme0e  36798  cdleme3g  36815  cdleme3h  36816  cdleme3  36818  cdleme5  36821  cdleme10  36835  cdleme11a  36841  cdleme11c  36842  cdleme11h  36847  cdleme11j  36848  cdleme0nex  36871  cdleme18a  36872  cdleme18b  36873  cdleme22gb  36875  cdleme20zN  36882  cdleme20c  36892  cdleme20k  36900  cdleme21a  36906  cdleme21b  36907  cdleme21c  36908  cdleme21h  36915  cdleme22b  36922  cdleme22d  36924  cdleme22f  36927  cdleme25a  36934  cdleme25c  36936  cdleme25dN  36937  cdleme26ee  36941  cdleme30a  36959  cdlemefr29bpre0N  36987  cdlemefr29clN  36988  cdlemefr32fvaN  36990  cdlemefr32fva1  36991  cdlemefs29bpre0N  36997  cdlemefs29bpre1N  36998  cdlemefs29cpre1N  36999  cdlemefs29clN  37000  cdleme43fsv1snlem  37001  cdlemefs32fvaN  37003  cdlemefs32fva1  37004  cdlemefs31fv1  37005  cdleme36a  37041  cdleme39a  37046  cdleme42a  37052  cdleme42c  37053  cdleme17d3  37077  cdleme48fv  37080  cdleme48bw  37083  cdleme48b  37084  cdlemeg46rgv  37109  cdlemeg46req  37110  cdlemeg46gfv  37111  cdleme48d  37116  cdleme50trn2a  37131  cdleme50trn2  37132  cdleme50ltrn  37138  cdlemf1  37142  cdlemf  37144  trlord  37150  cdlemg2dN  37171  cdlemg2fvlem  37175  cdlemg2l  37184  cdlemg7fvbwN  37188  cdlemg7aN  37206  cdlemg10bALTN  37217  cdlemg10c  37220  cdlemg17a  37242  cdlemg17dALTN  37245  cdlemg31b0a  37276  cdlemg31a  37278  cdlemg31b  37279  cdlemg34  37293  cdlemg36  37295  ltrnco  37300  trlcoabs2N  37303  trlcolem  37307  cdlemg48  37318  tgrpov  37329  tendoco2  37349  tendoplco2  37360  cdlemh1  37396  cdlemi1  37399  cdlemi2  37400  cdlemj3  37404  tendoid0  37406  cdlemk1  37412  cdlemk2  37413  cdlemk4  37415  cdlemk8  37419  cdlemk9  37420  cdlemk9bN  37421  cdlemk10  37424  cdlemk26b-3  37486  cdlemk26-3  37487  cdlemk28-3  37489  cdlemk37  37495  cdlemk39  37497  cdlemkfid1N  37502  cdlemkid1  37503  cdlemky  37507  cdlemkyu  37508  cdlemk19ylem  37511  cdlemk19xlem  37523  cdlemk11t  37527  cdlemk51  37534  cdlemkyyN  37543  cdleml6  37562  cdleml7  37563  cdleml8  37564  cdleml9  37565  erngdvlem4  37572  erngdvlem4-rN  37580  tendospcanN  37604  dia11N  37629  cdlemm10N  37699  dib11N  37741  dicvaddcl  37771  dicvscacl  37772  cdlemn6  37783  dihvalcq2  37828  dihopelvalcpre  37829  dihord6b  37841  dihord5apre  37843  dihmeetlem1N  37871  dihmeetlem2N  37880  dihglbcpreN  37881  dihjatc1  37892  dihmeetlem20N  37907  dih1dimatlem0  37909  dihatlat  37915  dihglblem6  37921  dochexmidlem4  38044  mapdpglem32  38286  mapdh8ad  38360  mapdh9aOLDN  38371  hdmap11lem2  38423  hdmap14lem6  38454  frlmfzowrdb  38580  mzpsubst  38740  pellex  38828  pellfundex  38879  pellfund14gap  38880  qirropth  38901  rmxypos  38940  congmul  38960  congsub  38963  mzpcong  38965  coprmdvdsb  38978  jm2.15nn0  38996  jm2.16nn0  38997  rpnnen3lem  39024  idomsubgmo  39194  relexp01min  39421  mullimc  41329  islptre  41332  limccog  41333  mullimcf  41336  addlimc  41361  0ellimcdiv  41362  limsupre3lem  41445  stoweidlem57  41774  fourierdlem48  41871  fourierdlem80  41903  fourierdlem113  41936  ovncvrrp  42278  opnvonmbllem2  42347  ovolval5lem3  42368  ovnovollem3  42372  itsclc0lem1  44112  itsclc0lem2  44113  itschlc0yqe  44116  itscnhlc0xyqsol  44121  itschlc0xyqsol1  44122