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

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

This theorem is referenced by:  simp13r  1290  simp23r  1296  simp33r  1302  f1oiso2  7327  tfisi  7835  tfrlem5  8348  omeulem1  8546  omeulem2  8547  elfiun  9381  isfin2-2  10272  addlid  11357  mulcan  11815  mulcan2  11816  divass  11855  divdir  11862  div11OLD  11866  ltdiv1  12047  ltmuldiv  12056  lediv2  12073  xaddass2  13210  xlt2add  13220  expaddz  14071  expmulz  14073  resqrex  15216  resqrtcl  15219  o1add  15580  o1mul  15581  o1sub  15582  dvdsgcd  16514  rpexp12i  16694  pythagtriplem4  16790  pythagtriplem11  16796  pythagtriplem13  16798  pcpremul  16814  pceu  16817  pcqmul  16824  pcqdiv  16828  f1ocpbllem  17487  funcoppc  17837  funcres  17858  catcisolem  18072  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  latjlej12  18414  latmlem12  18430  latj4  18448  latj4rot  18449  symgsssg  19397  symgfisg  19398  odcong  19479  cmn4  19731  ablsub4  19740  abladdsub4  19741  lsm4  19790  abvdom  20739  abvtrivd  20741  lspsolvlem  21052  lbsextlem2  21069  lidlsubcl  21134  frlmbas3  21685  matinvgcell  22322  matmulcell  22332  ma1repveval  22458  mdetunilem3  22501  mdetuni0  22508  mdetmul  22510  hausflimlem  23866  psmetlecl  24203  xmetlecl  24234  prdsxmetlem  24256  xblcntrps  24298  xblcntr  24299  bndth  24857  cph2ass  25113  iscau3  25178  dvres2  25813  coemullem  26155  vieta1  26220  aalioulem4  26243  cxpcn3lem  26657  angcan  26712  divsqrtsumlem  26890  dchrmusumlema  27404  dchrvmasumlema  27411  dchrisum0lema  27425  logdivsum  27444  padicabv  27541  cofcut1  27828  cofcut2  27830  divsmulw  28096  precsexlem8  28116  precsexlem9  28117  ax5seglem3  28858  ax5seglem6  28861  axpasch  28868  axeuclid  28890  axcontlem4  28894  axcontlem8  28898  trlsonistrl  29637  pthonispth  29676  spthonisspth  29680  wspthneq1eq2  29790  frgr2wwlkeqm  30260  adjlnop  32015  xreceu  32842  orngmul  33281  rhmdvd  33296  measvunilem  34202  measvuni  34204  bnj1128  34980  umgr2cycl  35128  satfv1fvfmla1  35410  cgrcomim  35977  cgrcoml  35984  cgrcomr  35985  cgrdegen  35992  segconeu  35999  btwnintr  36007  btwnexch3  36008  btwnouttr2  36010  btwnouttr  36012  btwnexch  36013  ifscgr  36032  lineext  36064  linecgr  36069  lineid  36071  idinside  36072  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem14  36088  btwnconn2  36090  btwnconn3  36091  midofsegid  36092  btwnoutside  36113  outsideoftr  36117  lineunray  36135  lineelsb2  36136  itg2addnclem  37665  cnres2  37757  heibor  37815  lsmcv2  39022  lcvat  39023  lcvexchlem4  39030  lcvexchlem5  39031  lfladd  39059  lflsub  39060  lflmul  39061  lshpkrlem4  39106  latm4  39226  omlmod1i2N  39253  cvlsupr7  39341  cvlsupr8  39342  hlatj4  39367  hlrelat3  39406  cvrval3  39407  atcvrj1  39425  atlelt  39432  2atlt  39433  2atjm  39439  3noncolr2  39443  athgt  39450  3dimlem2  39453  3dimlem4OLDN  39459  1cvratex  39467  ps-1  39471  ps-2  39472  hlatexch3N  39474  llnle  39512  atcvrlln2  39513  atcvrlln  39514  lplni2  39531  lplnle  39534  lplnnle2at  39535  lplnnlelln  39537  llncvrlpln2  39551  2llnmeqat  39565  lvolnle3at  39576  lvolnlelln  39578  4atlem0ae  39588  lneq2at  39772  lnjatN  39774  lncvrat  39776  2lnat  39778  elpaddri  39796  paddasslem2  39815  padd4N  39834  hlmod1i  39850  llnexchb2  39863  dalawlem2  39866  pclfinN  39894  pexmidlem4N  39967  pl42lem1N  39973  lhp2lt  39995  lhpexle1  40002  lhpexle2lem  40003  lhpj1  40016  lhpmcvr5N  40021  lhp2at0  40026  lhp2at0nle  40029  lhple  40036  lhpat  40037  lhpat4N  40038  4atexlemnslpq  40050  4atexlem7  40069  ltrn11  40120  ltrnle  40123  ltrnm  40125  ltrnj  40126  ltrncvr  40127  ltrnel  40133  ltrncnvel  40136  ltrncnv  40140  trlat  40163  trl0  40164  trlnidat  40167  trlnid  40173  ltrnatlw  40177  trlne  40179  trlval4  40182  cdlemc5  40189  cdlemd2  40193  cdlemd7  40198  cdlemd8  40199  cdlemd9  40200  cdleme0c  40207  cdleme0e  40211  cdleme0fN  40212  cdleme3g  40228  cdleme3h  40229  cdleme5  40234  cdleme11c  40255  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme0nex  40284  cdleme18a  40285  cdleme22gb  40288  cdleme20zN  40295  cdleme20c  40305  cdleme20k  40313  cdleme21a  40319  cdleme21b  40320  cdleme21c  40321  cdleme21ct  40323  cdleme21h  40328  cdleme22d  40337  cdleme22f  40340  cdleme26ee  40354  cdleme30a  40372  cdlemefs45eN  40425  cdleme36a  40454  cdleme36m  40455  cdleme39a  40459  cdleme42b  40472  cdleme43dN  40486  cdlemeg47rv2  40504  cdlemeg46sfg  40514  cdlemeg46rjgN  40516  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemeg46gfv  40524  cdleme48d  40529  cdleme50ltrn  40551  cdlemf1  40555  cdlemf  40557  cdlemg2dN  40584  cdlemg2fvlem  40588  cdlemg2l  40597  cdlemg7fvbwN  40601  cdlemg7aN  40619  cdlemg10c  40633  cdlemg17a  40655  cdlemg17dALTN  40658  cdlemg18a  40672  cdlemg18b  40673  cdlemg31b0a  40689  cdlemg31a  40691  cdlemg31b  40692  ltrnco  40713  cdlemg48  40731  tgrpov  40742  tendoco2  40762  tendoplco2  40773  cdlemh1  40809  cdlemk1  40825  cdlemk26b-3  40899  cdlemk27-3  40901  cdlemk28-3  40902  cdlemk34  40904  cdlemkfid1N  40915  cdlemkid3N  40927  cdlemkid4  40928  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk51  40947  tendospcanN  41017  cdlemm10N  41112  dicvaddcl  41184  dicvscacl  41185  cdlemn6  41196  dihvalcq2  41241  dihord6b  41254  dihord5apre  41256  dihglbcpreN  41294  dihjatc1  41305  dihmeetlem20N  41320  dih1dimatlem0  41322  dihglblem6  41334  dochexmidlem4  41457  mapdpglem32  41699  mapdh8ad  41773  mapdh9aOLDN  41784  hdmap11lem2  41836  hdmap14lem6  41867  frlmfzowrdb  42492  mzpmfp  42735  mzpsubst  42736  pellex  42823  pellfundex  42874  pellfund14gap  42875  qirropth  42896  rmxypos  42936  congmul  42956  congsub  42959  mzpcong  42961  coprmdvdsb  42974  jm2.15nn0  42992  jm2.16nn0  42993  rpnnen3lem  43020  idomsubgmo  43182  relexp01min  43702  mullimc  45614  islptre  45617  mullimcf  45621  addlimc  45646  0ellimcdiv  45647  limsupre3lem  45730  limsupre3uzlem  45733  fourierdlem48  46152  fourierdlem80  46184  opnvonmbllem2  46631  ovolval5lem3  46652  ovnovollem3  46656  difltmodne  47343  isubgr3stgrlem1  47965  mapprop  48334  lincfsuppcl  48402  lindslinindimp2lem3  48449  itsclc0lem1  48745  itsclc0lem2  48746  itschlc0yqe  48749  itsclc0xyqsolr  48758  swapffunc  49271  fucofunc  49348  fucoppc  49399