Theorem simp3r 1203

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3r	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 486	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1136	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simp13r  1290  simp23r  1296  simp33r  1302  f1oiso2  7346  tfisi  7845  tfrlem5  8377  omeulem1  8579  omeulem2  8580  elfiun  9422  isfin2-2  10311  addlid  11394  mulcan  11848  mulcan2  11849  divass  11887  divdir  11894  div11  11897  ltdiv1  12075  ltmuldiv  12084  lediv2  12101  xaddass2  13226  xlt2add  13236  expaddz  14069  expmulz  14071  resqrex  15194  resqrtcl  15197  o1add  15555  o1mul  15556  o1sub  15557  dvdsgcd  16483  rpexp12i  16658  pythagtriplem4  16749  pythagtriplem11  16755  pythagtriplem13  16757  pcpremul  16773  pceu  16776  pcqmul  16783  pcqdiv  16787  f1ocpbllem  17467  funcoppc  17822  funcres  17843  catcisolem  18057  1stfcl  18146  2ndfcl  18147  prfcl  18152  evlfcl  18172  curf1cl  18178  curfcl  18182  hofcl  18209  latjlej12  18405  latmlem12  18421  latj4  18439  latj4rot  18440  symgsssg  19330  symgfisg  19331  odcong  19412  cmn4  19664  ablsub4  19673  abladdsub4  19674  lsm4  19723  abvdom  20439  abvtrivd  20441  lspsolvlem  20748  lbsextlem2  20765  lidlsubcl  20832  frlmbas3  21323  matinvgcell  21929  matmulcell  21939  ma1repveval  22065  mdetunilem3  22108  mdetuni0  22115  mdetmul  22117  hausflimlem  23475  psmetlecl  23813  xmetlecl  23844  prdsxmetlem  23866  xblcntrps  23908  xblcntr  23909  bndth  24466  cph2ass  24722  iscau3  24787  dvres2  25421  coemullem  25756  vieta1  25817  aalioulem4  25840  cxpcn3lem  26245  angcan  26297  divsqrtsumlem  26474  dchrmusumlema  26986  dchrvmasumlema  26993  dchrisum0lema  27007  logdivsum  27026  padicabv  27123  cofcut1  27397  cofcut2  27399  divsmulw  27630  precsexlem8  27650  precsexlem9  27651  ax5seglem3  28179  ax5seglem6  28182  axpasch  28189  axeuclid  28211  axcontlem4  28215  axcontlem8  28219  trlsonistrl  28956  pthonispth  28993  spthonisspth  28997  wspthneq1eq2  29104  frgr2wwlkeqm  29574  adjlnop  31327  xreceu  32076  orngmul  32410  rhmdvd  32425  measvunilem  33199  measvuni  33201  bnj1128  33990  umgr2cycl  34121  satfv1fvfmla1  34403  cgrcomim  34950  cgrcoml  34957  cgrcomr  34958  cgrdegen  34965  segconeu  34972  btwnintr  34980  btwnexch3  34981  btwnouttr2  34983  btwnouttr  34985  btwnexch  34986  ifscgr  35005  lineext  35037  linecgr  35042  lineid  35044  idinside  35045  btwnconn1lem3  35050  btwnconn1lem4  35051  btwnconn1lem14  35061  btwnconn2  35063  btwnconn3  35064  midofsegid  35065  btwnoutside  35086  outsideoftr  35090  lineunray  35108  lineelsb2  35109  itg2addnclem  36528  cnres2  36620  heibor  36678  lsmcv2  37888  lcvat  37889  lcvexchlem4  37896  lcvexchlem5  37897  lfladd  37925  lflsub  37926  lflmul  37927  lshpkrlem4  37972  latm4  38092  omlmod1i2N  38119  cvlsupr7  38207  cvlsupr8  38208  hlatj4  38233  hlrelat3  38272  cvrval3  38273  atcvrj1  38291  atlelt  38298  2atlt  38299  2atjm  38305  3noncolr2  38309  athgt  38316  3dimlem2  38319  3dimlem4OLDN  38325  1cvratex  38333  ps-1  38337  ps-2  38338  hlatexch3N  38340  llnle  38378  atcvrlln2  38379  atcvrlln  38380  lplni2  38397  lplnle  38400  lplnnle2at  38401  lplnnlelln  38403  llncvrlpln2  38417  2llnmeqat  38431  lvolnle3at  38442  lvolnlelln  38444  4atlem0ae  38454  lneq2at  38638  lnjatN  38640  lncvrat  38642  2lnat  38644  elpaddri  38662  paddasslem2  38681  padd4N  38700  hlmod1i  38716  llnexchb2  38729  dalawlem2  38732  pclfinN  38760  pexmidlem4N  38833  pl42lem1N  38839  lhp2lt  38861  lhpexle1  38868  lhpexle2lem  38869  lhpj1  38882  lhpmcvr5N  38887  lhp2at0  38892  lhp2at0nle  38895  lhple  38902  lhpat  38903  lhpat4N  38904  4atexlemnslpq  38916  4atexlem7  38935  ltrn11  38986  ltrnle  38989  ltrnm  38991  ltrnj  38992  ltrncvr  38993  ltrnel  38999  ltrncnvel  39002  ltrncnv  39006  trlat  39029  trl0  39030  trlnidat  39033  trlnid  39039  ltrnatlw  39043  trlne  39045  trlval4  39048  cdlemc5  39055  cdlemd2  39059  cdlemd7  39064  cdlemd8  39065  cdlemd9  39066  cdleme0c  39073  cdleme0e  39077  cdleme0fN  39078  cdleme3g  39094  cdleme3h  39095  cdleme5  39100  cdleme11c  39121  cdleme11h  39126  cdleme11j  39127  cdleme11k  39128  cdleme0nex  39150  cdleme18a  39151  cdleme22gb  39154  cdleme20zN  39161  cdleme20c  39171  cdleme20k  39179  cdleme21a  39185  cdleme21b  39186  cdleme21c  39187  cdleme21ct  39189  cdleme21h  39194  cdleme22d  39203  cdleme22f  39206  cdleme26ee  39220  cdleme30a  39238  cdlemefs45eN  39291  cdleme36a  39320  cdleme36m  39321  cdleme39a  39325  cdleme42b  39338  cdleme43dN  39352  cdlemeg47rv2  39370  cdlemeg46sfg  39380  cdlemeg46rjgN  39382  cdlemeg46rgv  39388  cdlemeg46req  39389  cdlemeg46gfv  39390  cdleme48d  39395  cdleme50ltrn  39417  cdlemf1  39421  cdlemf  39423  cdlemg2dN  39450  cdlemg2fvlem  39454  cdlemg2l  39463  cdlemg7fvbwN  39467  cdlemg7aN  39485  cdlemg10c  39499  cdlemg17a  39521  cdlemg17dALTN  39524  cdlemg18a  39538  cdlemg18b  39539  cdlemg31b0a  39555  cdlemg31a  39557  cdlemg31b  39558  ltrnco  39579  cdlemg48  39597  tgrpov  39608  tendoco2  39628  tendoplco2  39639  cdlemh1  39675  cdlemk1  39691  cdlemk26b-3  39765  cdlemk27-3  39767  cdlemk28-3  39768  cdlemk34  39770  cdlemkfid1N  39781  cdlemkid3N  39793  cdlemkid4  39794  cdlemk35s-id  39798  cdlemk39s-id  39800  cdlemk51  39813  tendospcanN  39883  cdlemm10N  39978  dicvaddcl  40050  dicvscacl  40051  cdlemn6  40062  dihvalcq2  40107  dihord6b  40120  dihord5apre  40122  dihglbcpreN  40160  dihjatc1  40171  dihmeetlem20N  40186  dih1dimatlem0  40188  dihglblem6  40200  dochexmidlem4  40323  mapdpglem32  40565  mapdh8ad  40639  mapdh9aOLDN  40650  hdmap11lem2  40702  hdmap14lem6  40733  frlmfzowrdb  41076  mzpmfp  41471  mzpsubst  41472  pellex  41559  pellfundex  41610  pellfund14gap  41611  qirropth  41632  rmxypos  41672  congmul  41692  congsub  41695  mzpcong  41697  coprmdvdsb  41710  jm2.15nn0  41728  jm2.16nn0  41729  rpnnen3lem  41756  idomsubgmo  41926  relexp01min  42450  mullimc  44319  islptre  44322  mullimcf  44326  addlimc  44351  0ellimcdiv  44352  limsupre3lem  44435  limsupre3uzlem  44438  fourierdlem48  44857  fourierdlem80  44889  opnvonmbllem2  45336  ovolval5lem3  45357  ovnovollem3  45361  mapprop  46976  lincfsuppcl  47048  lindslinindimp2lem3  47095  itsclc0lem1  47396  itsclc0lem2  47397  itschlc0yqe  47400  itsclc0xyqsolr  47409