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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 397  df-3an 1088

This theorem is referenced by:  simp13l  1287  simp23l  1293  simp33l  1299  tfisi  7714  fpr3g  8110  tfrlem5  8220  omeulem1  8422  omeulem2  8423  uniinqs  8595  elfiun  9198  tcrank  9651  isfin2-2  10084  konigthlem  10333  gruen  10577  addid2  11167  mulcan  11621  mulcan2  11622  divass  11660  divdir  11667  div11  11670  muldivdir  11677  subdivcomb1  11679  subdivcomb2  11680  divcan5  11686  ltmul1  11834  ltdiv1  11848  ltmuldiv  11857  lediv2  11874  xaddass2  12993  xlt2add  13003  xmulasslem3  13029  xadddi2  13040  expaddz  13836  expmulz  13838  muldivbinom2  13986  resqrtcl  14974  o1add  15332  o1mul  15333  o1sub  15334  dvdsadd2b  16024  dvdsgcd  16261  rpexp12i  16438  pythagtriplem3  16528  pcpremul  16553  pceu  16556  pcqmul  16563  pcqdiv  16567  setsstruct  16886  f1ocpbllem  17244  funcoppc  17599  funcres  17620  catcisolem  17834  1stfcl  17923  2ndfcl  17924  prfcl  17929  evlfcl  17949  curf1cl  17955  curfcl  17959  hofcl  17986  latjlej12  18182  latmlem12  18198  latj4  18216  latj4rot  18217  symgsssg  19084  symgfisg  19085  psgnunilem4  19114  odcong  19166  cmn4  19415  ablsub4  19423  abladdsub4  19424  lsm4  19470  abvdom  20107  abvres  20108  abvtrivd  20109  lspsolvlem  20413  lbsextlem2  20430  lidlsubcl  20496  frlmbas3  20992  matmulcell  21603  marrepeval  21721  ma1repveval  21729  submaeval  21740  mdetunilem3  21772  mdetuni0  21779  mdetmul  21781  minmar1eval  21807  nllyrest  22646  hausflimlem  23139  tsmsxp  23315  psmetlecl  23477  xmetlecl  23508  prdsxmetlem  23530  ngpocelbl  23877  bndth  24130  cph2ass  24386  iscau3  24451  dvres2  25085  coemullem  25420  vieta1  25481  aalioulem4  25504  cxpcn3lem  25909  angcan  25961  dchrvmasumlema  26657  logdivsum  26690  abvcxp  26772  padicabv  26787  ax5seglem3  27308  ax5seglem6  27311  axpasch  27318  axeuclid  27340  axcontlem4  27344  axcontlem8  27348  wlkl1loop  28014  trlsonwlkon  28087  pthontrlon  28124  wspthsswwlknon  28295  frgr2wwlkeqm  28704  adjlnop  30457  xreceu  31205  orngmul  31511  rhmdvd  31529  measvunilem  32189  measvunilem0  32190  measres  32199  bnj1128  32979  umgr2cycllem  33111  umgr2cycl  33112  satfv1fvfmla1  33394  nosupbnd1lem4  33923  nosupbnd1lem5  33924  noinfbnd1lem4  33938  cofcut1  34099  cofcut2  34100  cgrcomim  34300  cgrcoml  34307  cgrcomr  34308  cgrdegen  34315  segconeu  34322  btwnintr  34330  btwnexch3  34331  btwnouttr2  34333  btwnouttr  34335  btwnexch  34336  trisegint  34339  lineext  34387  linecgr  34392  lineid  34394  idinside  34395  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem7  34404  btwnconn1lem14  34411  btwnconn2  34413  midofsegid  34415  btwnoutside  34436  outsideoftr  34440  lineunray  34458  lineelsb2  34459  cnres2  35930  heibor  35988  lsmcv2  37050  lcvat  37051  lcvexchlem4  37058  lcvexchlem5  37059  lfladd  37087  lflsub  37088  lflmul  37089  lshpkrlem4  37134  latm4  37254  omlmod1i2N  37281  cvlatexch3  37359  cvlsupr7  37369  hlatj4  37395  hlrelat3  37433  cvrval3  37434  atcvrj1  37452  atlelt  37459  2atlt  37460  2atjm  37466  3noncolr2  37470  athgt  37477  3dimlem2  37480  3dimlem4  37485  3dimlem4OLDN  37486  3dim3  37490  1cvratex  37494  ps-1  37498  ps-2  37499  hlatexch3N  37501  llnle  37539  atcvrlln2  37540  atcvrlln  37541  lplni2  37558  lplnle  37561  lplnnle2at  37562  llncvrlpln2  37578  lplnexllnN  37585  2llnmeqat  37592  lvolnle3at  37603  4atlem0ae  37615  lplncvrlvol2  37636  lnjatN  37801  lncvrat  37803  cdlemblem  37814  elpaddri  37823  paddasslem2  37842  paddasslem16  37856  padd4N  37861  hlmod1i  37877  dalawlem2  37893  pclfinN  37921  pexmidlem4N  37994  pl42lem1N  38000  lhp2lt  38022  lhpexle1  38029  lhpexle2lem  38030  lhpj1  38043  lhpmcvr5N  38048  lhp2at0  38053  lhp2atnle  38054  lhp2at0nle  38056  lhple  38063  lhpat  38064  lhpat4N  38065  4atexlempnq  38076  4atexlem7  38096  4atex  38097  ltrn11  38147  ltrnle  38150  ltrnm  38152  ltrnj  38153  ltrncvr  38154  ltrnel  38160  ltrncnvel  38163  ltrncnv  38167  trlval2  38184  trlcnv  38186  trljat1  38187  trljat2  38188  trlat  38190  trl0  38191  trlnidat  38194  trlnid  38200  cdlemc1  38212  cdlemc2  38213  cdlemc5  38216  cdlemd2  38220  cdlemd7  38225  cdlemd8  38226  cdlemd9  38227  cdleme0e  38238  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme5  38261  cdleme10  38275  cdleme11a  38281  cdleme11c  38282  cdleme11h  38287  cdleme11j  38288  cdleme0nex  38311  cdleme18a  38312  cdleme18b  38313  cdleme22gb  38315  cdleme20zN  38322  cdleme20c  38332  cdleme20k  38340  cdleme21a  38346  cdleme21b  38347  cdleme21c  38348  cdleme21h  38355  cdleme22b  38362  cdleme22d  38364  cdleme22f  38367  cdleme25a  38374  cdleme25c  38376  cdleme25dN  38377  cdleme26ee  38381  cdleme30a  38399  cdlemefr29bpre0N  38427  cdlemefr29clN  38428  cdlemefr32fvaN  38430  cdlemefr32fva1  38431  cdlemefs29bpre0N  38437  cdlemefs29bpre1N  38438  cdlemefs29cpre1N  38439  cdlemefs29clN  38440  cdleme43fsv1snlem  38441  cdlemefs32fvaN  38443  cdlemefs32fva1  38444  cdlemefs31fv1  38445  cdleme36a  38481  cdleme39a  38486  cdleme42a  38492  cdleme42c  38493  cdleme17d3  38517  cdleme48fv  38520  cdleme48bw  38523  cdleme48b  38524  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemeg46gfv  38551  cdleme48d  38556  cdleme50trn2a  38571  cdleme50trn2  38572  cdleme50ltrn  38578  cdlemf1  38582  cdlemf  38584  trlord  38590  cdlemg2dN  38611  cdlemg2fvlem  38615  cdlemg2l  38624  cdlemg7fvbwN  38628  cdlemg7aN  38646  cdlemg10bALTN  38657  cdlemg10c  38660  cdlemg17a  38682  cdlemg17dALTN  38685  cdlemg31b0a  38716  cdlemg31a  38718  cdlemg31b  38719  cdlemg34  38733  cdlemg36  38735  ltrnco  38740  trlcoabs2N  38743  trlcolem  38747  cdlemg48  38758  tgrpov  38769  tendoco2  38789  tendoplco2  38800  cdlemh1  38836  cdlemi1  38839  cdlemi2  38840  cdlemj3  38844  tendoid0  38846  cdlemk1  38852  cdlemk2  38853  cdlemk4  38855  cdlemk8  38859  cdlemk9  38860  cdlemk9bN  38861  cdlemk10  38864  cdlemk26b-3  38926  cdlemk26-3  38927  cdlemk28-3  38929  cdlemk37  38935  cdlemk39  38937  cdlemkfid1N  38942  cdlemkid1  38943  cdlemky  38947  cdlemkyu  38948  cdlemk19ylem  38951  cdlemk19xlem  38963  cdlemk11t  38967  cdlemk51  38974  cdlemkyyN  38983  cdleml6  39002  cdleml7  39003  cdleml8  39004  cdleml9  39005  erngdvlem4  39012  erngdvlem4-rN  39020  tendospcanN  39044  dia11N  39069  cdlemm10N  39139  dib11N  39181  dicvaddcl  39211  dicvscacl  39212  cdlemn6  39223  dihvalcq2  39268  dihopelvalcpre  39269  dihord6b  39281  dihord5apre  39283  dihmeetlem1N  39311  dihmeetlem2N  39320  dihglbcpreN  39321  dihjatc1  39332  dihmeetlem20N  39347  dih1dimatlem0  39349  dihatlat  39355  dihglblem6  39361  dochexmidlem4  39484  mapdpglem32  39726  mapdh8ad  39800  mapdh9aOLDN  39811  hdmap11lem2  39863  hdmap14lem6  39894  frlmfzowrdb  40242  flt4lem5  40494  mzpsubst  40577  pellex  40664  pellfundex  40715  pellfund14gap  40716  qirropth  40737  rmxypos  40776  congmul  40796  congsub  40799  mzpcong  40801  coprmdvdsb  40814  jm2.15nn0  40832  jm2.16nn0  40833  rpnnen3lem  40860  idomsubgmo  41030  relexp01min  41328  mullimc  43164  islptre  43167  limccog  43168  mullimcf  43171  addlimc  43196  0ellimcdiv  43197  limsupre3lem  43280  stoweidlem57  43605  fourierdlem48  43702  fourierdlem80  43734  fourierdlem113  43767  ovncvrrp  44109  opnvonmbllem2  44178  ovolval5lem3  44199  ovnovollem3  44203  itsclc0lem1  46113  itsclc0lem2  46114  itschlc0yqe  46117  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123