Theorem simp3l 1082

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl3l  1109  simpr3l  1115  simp13l  1169  simp23l  1175  simp33l  1181  tfisi  6950  tfrlem5  7363  omeulem1  7549  omeulem2  7550  uniinqs  7714  elfiun  8219  tcrank  8630  isfin2-2  9024  konigthlem  9269  gruen  9513  addid2  10098  mulcan  10543  mulcan2  10544  divass  10582  divdir  10589  div11  10592  muldivdir  10599  divcan5  10606  ltmul1  10752  ltdiv1  10766  ltmuldiv  10775  lediv2  10792  xaddass2  11952  xlt2add  11962  xmulasslem3  11988  xadddi2  11999  expaddz  12766  expmulz  12768  muldivbinom2  12909  resqrtcl  13842  o1add  14192  o1mul  14193  o1sub  14194  dvdsadd2b  14866  dvdsgcd  15099  rpexp12i  15272  pythagtriplem3  15361  pcpremul  15386  pceu  15389  pcqmul  15396  pcqdiv  15400  f1ocpbllem  16007  funcoppc  16358  funcres  16379  catcisolem  16579  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  curfcl  16695  hofcl  16722  latjlej12  16890  latmlem12  16906  latj4  16924  latj4rot  16925  symgsssg  17710  symgfisg  17711  psgnunilem4  17740  odcong  17791  cmn4  18035  ablsub4  18041  abladdsub4  18042  lsm4  18086  abvdom  18661  abvres  18662  abvtrivd  18663  lspsolvlem  18963  lbsextlem2  18980  lidlsubcl  19037  frlmbas3  19934  matmulcell  20070  marrepeval  20188  ma1repveval  20196  submaeval  20207  mdetunilem3  20239  mdetuni0  20246  mdetmul  20248  minmar1eval  20274  nllyrest  21099  hausflimlem  21593  tsmsxp  21768  psmetlecl  21930  xmetlecl  21961  prdsxmetlem  21983  ngpocelbl  22318  bndth  22565  cph2ass  22821  iscau3  22884  dvres2  23482  coemullem  23810  vieta1  23871  aalioulem4  23894  cxpcn3lem  24288  angcan  24332  dchrvmasumlema  24989  logdivsum  25022  abvcxp  25104  padicabv  25119  ax5seglem3  25611  ax5seglem6  25614  axpasch  25621  axeuclid  25643  axcontlem4  25647  axcontlem8  25651  clwwlknimp  26304  adjlnop  28329  xreceu  28961  orngmul  29134  rhmdvd  29152  measvunilem  29602  measvunilem0  29603  measres  29612  bnj1128  30312  subdivcomb1  30864  subdivcomb2  30865  cgrcomim  31266  cgrcoml  31273  cgrcomr  31274  cgrdegen  31281  segconeu  31288  btwnintr  31296  btwnexch3  31297  btwnouttr2  31299  btwnouttr  31301  btwnexch  31302  trisegint  31305  lineext  31353  linecgr  31358  lineid  31360  idinside  31361  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem7  31370  btwnconn1lem14  31377  btwnconn2  31379  midofsegid  31381  btwnoutside  31402  outsideoftr  31406  lineunray  31424  lineelsb2  31425  cnres2  32732  heibor  32790  lsmcv2  33334  lcvat  33335  lcvexchlem4  33342  lcvexchlem5  33343  lfladd  33371  lflsub  33372  lflmul  33373  lshpkrlem4  33418  latm4  33538  omlmod1i2N  33565  cvlatexch3  33643  cvlsupr7  33653  hlatj4  33678  hlrelat3  33716  cvrval3  33717  atcvrj1  33735  atlelt  33742  2atlt  33743  2atjm  33749  3noncolr2  33753  athgt  33760  3dimlem2  33763  3dimlem4  33768  3dimlem4OLDN  33769  3dim3  33773  1cvratex  33777  ps-1  33781  ps-2  33782  hlatexch3N  33784  llnle  33822  atcvrlln2  33823  atcvrlln  33824  lplni2  33841  lplnle  33844  lplnnle2at  33845  llncvrlpln2  33861  lplnexllnN  33868  2llnmeqat  33875  lvolnle3at  33886  4atlem0ae  33898  lplncvrlvol2  33919  lnjatN  34084  lncvrat  34086  cdlemblem  34097  elpaddri  34106  paddasslem2  34125  paddasslem16  34139  padd4N  34144  hlmod1i  34160  dalawlem2  34176  pclfinN  34204  pexmidlem4N  34277  pl42lem1N  34283  lhp2lt  34305  lhpexle1  34312  lhpexle2lem  34313  lhpj1  34326  lhpmcvr5N  34331  lhp2at0  34336  lhp2atnle  34337  lhp2at0nle  34339  lhple  34346  lhpat  34347  lhpat4N  34348  4atexlempnq  34359  4atexlem7  34379  4atex  34380  ltrn11  34430  ltrnle  34433  ltrnm  34435  ltrnj  34436  ltrncvr  34437  ltrnel  34443  ltrncnvel  34446  ltrncnv  34450  ltrnmwOLD  34456  trlval2  34468  trlcnv  34470  trljat1  34471  trljat2  34472  trlat  34474  trl0  34475  trlnidat  34478  trlnid  34484  cdlemc1  34496  cdlemc2  34497  cdlemc5  34500  cdlemd2  34504  cdlemd7  34509  cdlemd8  34510  cdlemd9  34511  cdleme0e  34522  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme5  34545  cdleme10  34559  cdleme11a  34565  cdleme11c  34566  cdleme11h  34571  cdleme11j  34572  cdleme0nex  34595  cdleme18a  34596  cdleme18b  34597  cdleme22gb  34599  cdleme20zN  34606  cdleme20yOLD  34608  cdleme20c  34617  cdleme20k  34625  cdleme21a  34631  cdleme21b  34632  cdleme21c  34633  cdleme21h  34640  cdleme22b  34647  cdleme22d  34649  cdleme22f  34652  cdleme25a  34659  cdleme25c  34661  cdleme25dN  34662  cdleme26ee  34666  cdleme30a  34684  cdlemefr29bpre0N  34712  cdlemefr29clN  34713  cdlemefr32fvaN  34715  cdlemefr32fva1  34716  cdlemefs29bpre0N  34722  cdlemefs29bpre1N  34723  cdlemefs29cpre1N  34724  cdlemefs29clN  34725  cdleme43fsv1snlem  34726  cdlemefs32fvaN  34728  cdlemefs32fva1  34729  cdlemefs31fv1  34730  cdleme36a  34766  cdleme39a  34771  cdleme42a  34777  cdleme42c  34778  cdleme17d3  34802  cdleme48fv  34805  cdleme48bw  34808  cdleme48b  34809  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemeg46gfv  34836  cdleme48d  34841  cdleme50trn2a  34856  cdleme50trn2  34857  cdleme50ltrn  34863  cdlemf1  34867  cdlemf  34869  trlord  34875  cdlemg2dN  34896  cdlemg2fvlem  34900  cdlemg2l  34909  cdlemg7fvbwN  34913  cdlemg7aN  34931  cdlemg10bALTN  34942  cdlemg10c  34945  cdlemg17a  34967  cdlemg17dALTN  34970  cdlemg31b0a  35001  cdlemg31a  35003  cdlemg31b  35004  cdlemg34  35018  cdlemg36  35020  ltrnco  35025  trlcoabs2N  35028  trlcolem  35032  cdlemg48  35043  tgrpov  35054  tendoco2  35074  tendoplco2  35085  cdlemh1  35121  cdlemi1  35124  cdlemi2  35125  cdlemj3  35129  tendoid0  35131  cdlemk1  35137  cdlemk2  35138  cdlemk4  35140  cdlemk8  35144  cdlemk9  35145  cdlemk9bN  35146  cdlemk10  35149  cdlemk26b-3  35211  cdlemk26-3  35212  cdlemk28-3  35214  cdlemk37  35220  cdlemk39  35222  cdlemkfid1N  35227  cdlemkid1  35228  cdlemky  35232  cdlemkyu  35233  cdlemk19ylem  35236  cdlemk19xlem  35248  cdlemk11t  35252  cdlemk51  35259  cdlemkyyN  35268  cdleml6  35287  cdleml7  35288  cdleml8  35289  cdleml9  35290  erngdvlem4  35297  erngdvlem4-rN  35305  tendospcanN  35330  dia11N  35355  cdlemm10N  35425  dib11N  35467  dicvaddcl  35497  dicvscacl  35498  cdlemn6  35509  dihvalcq2  35554  dihopelvalcpre  35555  dihord6b  35567  dihord5apre  35569  dihmeetlem1N  35597  dihmeetlem2N  35606  dihglbcpreN  35607  dihjatc1  35618  dihmeetlem20N  35633  dih1dimatlem0  35635  dihatlat  35641  dihglblem6  35647  dochexmidlem4  35770  mapdpglem32  36012  mapdh8ad  36086  mapdh9aOLDN  36098  hdmap11lem2  36152  hdmap14lem6  36183  mzpsubst  36329  pellex  36417  pellfundex  36468  pellfund14gap  36469  qirropth  36491  rmxypos  36532  congmul  36552  congsub  36555  mzpcong  36557  coprmdvdsb  36570  jm2.15nn0  36588  jm2.16nn0  36589  rpnnen3lem  36616  idomsubgmo  36795  relexp01min  37024  mullimc  38683  islptre  38686  limccog  38687  mullimcf  38690  addlimc  38715  0ellimcdiv  38716  stoweidlem57  38950  fourierdlem48  39047  fourierdlem80  39079  fourierdlem113  39112  ovncvrrp  39454  opnvonmbllem2  39523  ovolval5lem3  39544  ovnovollem3  39548  1wlkl1loop  40842  trlsonwlkon  40917  pthontrlon  40953  wspthsswwlknon  41128