Theorem simp3l 1197

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp13l  1284  simp23l  1290  simp33l  1296  tfisi  7572  tfrlem5  8015  omeulem1  8207  omeulem2  8208  uniinqs  8376  elfiun  8893  tcrank  9312  isfin2-2  9740  konigthlem  9989  gruen  10233  addid2  10822  mulcan  11276  mulcan2  11277  divass  11315  divdir  11322  div11  11325  muldivdir  11332  subdivcomb1  11334  subdivcomb2  11335  divcan5  11341  ltmul1  11489  ltdiv1  11503  ltmuldiv  11512  lediv2  11529  xaddass2  12642  xlt2add  12652  xmulasslem3  12678  xadddi2  12689  expaddz  13472  expmulz  13474  muldivbinom2  13622  resqrtcl  14612  o1add  14969  o1mul  14970  o1sub  14971  dvdsadd2b  15655  dvdsgcd  15891  rpexp12i  16065  pythagtriplem3  16154  pcpremul  16179  pceu  16182  pcqmul  16189  pcqdiv  16193  setsstruct  16522  f1ocpbllem  16796  funcoppc  17144  funcres  17165  catcisolem  17365  1stfcl  17446  2ndfcl  17447  prfcl  17452  evlfcl  17471  curf1cl  17477  curfcl  17481  hofcl  17508  latjlej12  17676  latmlem12  17692  latj4  17710  latj4rot  17711  symgsssg  18594  symgfisg  18595  psgnunilem4  18624  odcong  18676  cmn4  18925  ablsub4  18932  abladdsub4  18933  lsm4  18979  abvdom  19608  abvres  19609  abvtrivd  19610  lspsolvlem  19913  lbsextlem2  19930  lidlsubcl  19988  frlmbas3  20919  matmulcell  21053  marrepeval  21171  ma1repveval  21179  submaeval  21190  mdetunilem3  21222  mdetuni0  21229  mdetmul  21231  minmar1eval  21257  nllyrest  22093  hausflimlem  22586  tsmsxp  22762  psmetlecl  22924  xmetlecl  22955  prdsxmetlem  22977  ngpocelbl  23312  bndth  23561  cph2ass  23816  iscau3  23880  dvres2  24509  coemullem  24839  vieta1  24900  aalioulem4  24923  cxpcn3lem  25327  angcan  25379  dchrvmasumlema  26075  logdivsum  26108  abvcxp  26190  padicabv  26205  ax5seglem3  26716  ax5seglem6  26719  axpasch  26726  axeuclid  26748  axcontlem4  26752  axcontlem8  26756  wlkl1loop  27418  trlsonwlkon  27490  pthontrlon  27527  wspthsswwlknon  27699  frgr2wwlkeqm  28109  adjlnop  29862  xreceu  30598  orngmul  30876  rhmdvd  30894  measvunilem  31471  measvunilem0  31472  measres  31481  bnj1128  32262  umgr2cycllem  32387  umgr2cycl  32388  satfv1fvfmla1  32670  fpr3g  33122  nosupbnd1lem4  33211  nosupbnd1lem5  33212  cgrcomim  33450  cgrcoml  33457  cgrcomr  33458  cgrdegen  33465  segconeu  33472  btwnintr  33480  btwnexch3  33481  btwnouttr2  33483  btwnouttr  33485  btwnexch  33486  trisegint  33489  lineext  33537  linecgr  33542  lineid  33544  idinside  33545  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem7  33554  btwnconn1lem14  33561  btwnconn2  33563  midofsegid  33565  btwnoutside  33586  outsideoftr  33590  lineunray  33608  lineelsb2  33609  cnres2  35040  heibor  35098  lsmcv2  36164  lcvat  36165  lcvexchlem4  36172  lcvexchlem5  36173  lfladd  36201  lflsub  36202  lflmul  36203  lshpkrlem4  36248  latm4  36368  omlmod1i2N  36395  cvlatexch3  36473  cvlsupr7  36483  hlatj4  36509  hlrelat3  36547  cvrval3  36548  atcvrj1  36566  atlelt  36573  2atlt  36574  2atjm  36580  3noncolr2  36584  athgt  36591  3dimlem2  36594  3dimlem4  36599  3dimlem4OLDN  36600  3dim3  36604  1cvratex  36608  ps-1  36612  ps-2  36613  hlatexch3N  36615  llnle  36653  atcvrlln2  36654  atcvrlln  36655  lplni2  36672  lplnle  36675  lplnnle2at  36676  llncvrlpln2  36692  lplnexllnN  36699  2llnmeqat  36706  lvolnle3at  36717  4atlem0ae  36729  lplncvrlvol2  36750  lnjatN  36915  lncvrat  36917  cdlemblem  36928  elpaddri  36937  paddasslem2  36956  paddasslem16  36970  padd4N  36975  hlmod1i  36991  dalawlem2  37007  pclfinN  37035  pexmidlem4N  37108  pl42lem1N  37114  lhp2lt  37136  lhpexle1  37143  lhpexle2lem  37144  lhpj1  37157  lhpmcvr5N  37162  lhp2at0  37167  lhp2atnle  37168  lhp2at0nle  37170  lhple  37177  lhpat  37178  lhpat4N  37179  4atexlempnq  37190  4atexlem7  37210  4atex  37211  ltrn11  37261  ltrnle  37264  ltrnm  37266  ltrnj  37267  ltrncvr  37268  ltrnel  37274  ltrncnvel  37277  ltrncnv  37281  trlval2  37298  trlcnv  37300  trljat1  37301  trljat2  37302  trlat  37304  trl0  37305  trlnidat  37308  trlnid  37314  cdlemc1  37326  cdlemc2  37327  cdlemc5  37330  cdlemd2  37334  cdlemd7  37339  cdlemd8  37340  cdlemd9  37341  cdleme0e  37352  cdleme3g  37369  cdleme3h  37370  cdleme3  37372  cdleme5  37375  cdleme10  37389  cdleme11a  37395  cdleme11c  37396  cdleme11h  37401  cdleme11j  37402  cdleme0nex  37425  cdleme18a  37426  cdleme18b  37427  cdleme22gb  37429  cdleme20zN  37436  cdleme20c  37446  cdleme20k  37454  cdleme21a  37460  cdleme21b  37461  cdleme21c  37462  cdleme21h  37469  cdleme22b  37476  cdleme22d  37478  cdleme22f  37481  cdleme25a  37488  cdleme25c  37490  cdleme25dN  37491  cdleme26ee  37495  cdleme30a  37513  cdlemefr29bpre0N  37541  cdlemefr29clN  37542  cdlemefr32fvaN  37544  cdlemefr32fva1  37545  cdlemefs29bpre0N  37551  cdlemefs29bpre1N  37552  cdlemefs29cpre1N  37553  cdlemefs29clN  37554  cdleme43fsv1snlem  37555  cdlemefs32fvaN  37557  cdlemefs32fva1  37558  cdlemefs31fv1  37559  cdleme36a  37595  cdleme39a  37600  cdleme42a  37606  cdleme42c  37607  cdleme17d3  37631  cdleme48fv  37634  cdleme48bw  37637  cdleme48b  37638  cdlemeg46rgv  37663  cdlemeg46req  37664  cdlemeg46gfv  37665  cdleme48d  37670  cdleme50trn2a  37685  cdleme50trn2  37686  cdleme50ltrn  37692  cdlemf1  37696  cdlemf  37698  trlord  37704  cdlemg2dN  37725  cdlemg2fvlem  37729  cdlemg2l  37738  cdlemg7fvbwN  37742  cdlemg7aN  37760  cdlemg10bALTN  37771  cdlemg10c  37774  cdlemg17a  37796  cdlemg17dALTN  37799  cdlemg31b0a  37830  cdlemg31a  37832  cdlemg31b  37833  cdlemg34  37847  cdlemg36  37849  ltrnco  37854  trlcoabs2N  37857  trlcolem  37861  cdlemg48  37872  tgrpov  37883  tendoco2  37903  tendoplco2  37914  cdlemh1  37950  cdlemi1  37953  cdlemi2  37954  cdlemj3  37958  tendoid0  37960  cdlemk1  37966  cdlemk2  37967  cdlemk4  37969  cdlemk8  37973  cdlemk9  37974  cdlemk9bN  37975  cdlemk10  37978  cdlemk26b-3  38040  cdlemk26-3  38041  cdlemk28-3  38043  cdlemk37  38049  cdlemk39  38051  cdlemkfid1N  38056  cdlemkid1  38057  cdlemky  38061  cdlemkyu  38062  cdlemk19ylem  38065  cdlemk19xlem  38077  cdlemk11t  38081  cdlemk51  38088  cdlemkyyN  38097  cdleml6  38116  cdleml7  38117  cdleml8  38118  cdleml9  38119  erngdvlem4  38126  erngdvlem4-rN  38134  tendospcanN  38158  dia11N  38183  cdlemm10N  38253  dib11N  38295  dicvaddcl  38325  dicvscacl  38326  cdlemn6  38337  dihvalcq2  38382  dihopelvalcpre  38383  dihord6b  38395  dihord5apre  38397  dihmeetlem1N  38425  dihmeetlem2N  38434  dihglbcpreN  38435  dihjatc1  38446  dihmeetlem20N  38461  dih1dimatlem0  38463  dihatlat  38469  dihglblem6  38475  dochexmidlem4  38598  mapdpglem32  38840  mapdh8ad  38914  mapdh9aOLDN  38925  hdmap11lem2  38977  hdmap14lem6  39008  frlmfzowrdb  39141  mzpsubst  39343  pellex  39430  pellfundex  39481  pellfund14gap  39482  qirropth  39503  rmxypos  39542  congmul  39562  congsub  39565  mzpcong  39567  coprmdvdsb  39580  jm2.15nn0  39598  jm2.16nn0  39599  rpnnen3lem  39626  idomsubgmo  39796  relexp01min  40056  mullimc  41895  islptre  41898  limccog  41899  mullimcf  41902  addlimc  41927  0ellimcdiv  41928  limsupre3lem  42011  stoweidlem57  42341  fourierdlem48  42438  fourierdlem80  42470  fourierdlem113  42503  ovncvrrp  42845  opnvonmbllem2  42914  ovolval5lem3  42935  ovnovollem3  42939  itsclc0lem1  44742  itsclc0lem2  44743  itschlc0yqe  44746  itscnhlc0xyqsol  44751  itschlc0xyqsol1  44752