Theorem simp3r 1201

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 485	. 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:  simp13r  1288  simp23r  1294  simp33r  1300  f1oiso2  7232  tfisi  7714  tfrlem5  8220  omeulem1  8422  omeulem2  8423  elfiun  9198  isfin2-2  10084  addid2  11167  mulcan  11621  mulcan2  11622  divass  11660  divdir  11667  div11  11670  ltdiv1  11848  ltmuldiv  11857  lediv2  11874  xaddass2  12993  xlt2add  13003  expaddz  13836  expmulz  13838  resqrex  14971  resqrtcl  14974  o1add  15332  o1mul  15333  o1sub  15334  dvdsgcd  16261  rpexp12i  16438  pythagtriplem4  16529  pythagtriplem11  16535  pythagtriplem13  16537  pcpremul  16553  pceu  16556  pcqmul  16563  pcqdiv  16567  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  odcong  19166  cmn4  19415  ablsub4  19423  abladdsub4  19424  lsm4  19470  abvdom  20107  abvtrivd  20109  lspsolvlem  20413  lbsextlem2  20430  lidlsubcl  20496  frlmbas3  20992  matinvgcell  21593  matmulcell  21603  ma1repveval  21729  mdetunilem3  21772  mdetuni0  21779  mdetmul  21781  hausflimlem  23139  psmetlecl  23477  xmetlecl  23508  prdsxmetlem  23530  xblcntrps  23572  xblcntr  23573  bndth  24130  cph2ass  24386  iscau3  24451  dvres2  25085  coemullem  25420  vieta1  25481  aalioulem4  25504  cxpcn3lem  25909  angcan  25961  divsqrtsumlem  26138  dchrmusumlema  26650  dchrvmasumlema  26657  dchrisum0lema  26671  logdivsum  26690  padicabv  26787  ax5seglem3  27308  ax5seglem6  27311  axpasch  27318  axeuclid  27340  axcontlem4  27344  axcontlem8  27348  trlsonistrl  28086  pthonispth  28123  spthonisspth  28127  wspthneq1eq2  28234  frgr2wwlkeqm  28704  adjlnop  30457  xreceu  31205  orngmul  31511  rhmdvd  31529  measvunilem  32189  measvuni  32191  bnj1128  32979  umgr2cycl  33112  satfv1fvfmla1  33394  cofcut1  34099  cofcut2  34100  cgrcomim  34300  cgrcoml  34307  cgrcomr  34308  cgrdegen  34315  segconeu  34322  btwnintr  34330  btwnexch3  34331  btwnouttr2  34333  btwnouttr  34335  btwnexch  34336  ifscgr  34355  lineext  34387  linecgr  34392  lineid  34394  idinside  34395  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem14  34411  btwnconn2  34413  btwnconn3  34414  midofsegid  34415  btwnoutside  34436  outsideoftr  34440  lineunray  34458  lineelsb2  34459  itg2addnclem  35837  cnres2  35930  heibor  35988  lsmcv2  37050  lcvat  37051  lcvexchlem4  37058  lcvexchlem5  37059  lfladd  37087  lflsub  37088  lflmul  37089  lshpkrlem4  37134  latm4  37254  omlmod1i2N  37281  cvlsupr7  37369  cvlsupr8  37370  hlatj4  37395  hlrelat3  37433  cvrval3  37434  atcvrj1  37452  atlelt  37459  2atlt  37460  2atjm  37466  3noncolr2  37470  athgt  37477  3dimlem2  37480  3dimlem4OLDN  37486  1cvratex  37494  ps-1  37498  ps-2  37499  hlatexch3N  37501  llnle  37539  atcvrlln2  37540  atcvrlln  37541  lplni2  37558  lplnle  37561  lplnnle2at  37562  lplnnlelln  37564  llncvrlpln2  37578  2llnmeqat  37592  lvolnle3at  37603  lvolnlelln  37605  4atlem0ae  37615  lneq2at  37799  lnjatN  37801  lncvrat  37803  2lnat  37805  elpaddri  37823  paddasslem2  37842  padd4N  37861  hlmod1i  37877  llnexchb2  37890  dalawlem2  37893  pclfinN  37921  pexmidlem4N  37994  pl42lem1N  38000  lhp2lt  38022  lhpexle1  38029  lhpexle2lem  38030  lhpj1  38043  lhpmcvr5N  38048  lhp2at0  38053  lhp2at0nle  38056  lhple  38063  lhpat  38064  lhpat4N  38065  4atexlemnslpq  38077  4atexlem7  38096  ltrn11  38147  ltrnle  38150  ltrnm  38152  ltrnj  38153  ltrncvr  38154  ltrnel  38160  ltrncnvel  38163  ltrncnv  38167  trlat  38190  trl0  38191  trlnidat  38194  trlnid  38200  ltrnatlw  38204  trlne  38206  trlval4  38209  cdlemc5  38216  cdlemd2  38220  cdlemd7  38225  cdlemd8  38226  cdlemd9  38227  cdleme0c  38234  cdleme0e  38238  cdleme0fN  38239  cdleme3g  38255  cdleme3h  38256  cdleme5  38261  cdleme11c  38282  cdleme11h  38287  cdleme11j  38288  cdleme11k  38289  cdleme0nex  38311  cdleme18a  38312  cdleme22gb  38315  cdleme20zN  38322  cdleme20c  38332  cdleme20k  38340  cdleme21a  38346  cdleme21b  38347  cdleme21c  38348  cdleme21ct  38350  cdleme21h  38355  cdleme22d  38364  cdleme22f  38367  cdleme26ee  38381  cdleme30a  38399  cdlemefs45eN  38452  cdleme36a  38481  cdleme36m  38482  cdleme39a  38486  cdleme42b  38499  cdleme43dN  38513  cdlemeg47rv2  38531  cdlemeg46sfg  38541  cdlemeg46rjgN  38543  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemeg46gfv  38551  cdleme48d  38556  cdleme50ltrn  38578  cdlemf1  38582  cdlemf  38584  cdlemg2dN  38611  cdlemg2fvlem  38615  cdlemg2l  38624  cdlemg7fvbwN  38628  cdlemg7aN  38646  cdlemg10c  38660  cdlemg17a  38682  cdlemg17dALTN  38685  cdlemg18a  38699  cdlemg18b  38700  cdlemg31b0a  38716  cdlemg31a  38718  cdlemg31b  38719  ltrnco  38740  cdlemg48  38758  tgrpov  38769  tendoco2  38789  tendoplco2  38800  cdlemh1  38836  cdlemk1  38852  cdlemk26b-3  38926  cdlemk27-3  38928  cdlemk28-3  38929  cdlemk34  38931  cdlemkfid1N  38942  cdlemkid3N  38954  cdlemkid4  38955  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk51  38974  tendospcanN  39044  cdlemm10N  39139  dicvaddcl  39211  dicvscacl  39212  cdlemn6  39223  dihvalcq2  39268  dihord6b  39281  dihord5apre  39283  dihglbcpreN  39321  dihjatc1  39332  dihmeetlem20N  39347  dih1dimatlem0  39349  dihglblem6  39361  dochexmidlem4  39484  mapdpglem32  39726  mapdh8ad  39800  mapdh9aOLDN  39811  hdmap11lem2  39863  hdmap14lem6  39894  frlmfzowrdb  40242  mzpmfp  40576  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  mullimcf  43171  addlimc  43196  0ellimcdiv  43197  limsupre3lem  43280  limsupre3uzlem  43283  fourierdlem48  43702  fourierdlem80  43734  opnvonmbllem2  44178  ovolval5lem3  44199  ovnovollem3  44203  mapprop  45693  lincfsuppcl  45765  lindslinindimp2lem3  45812  itsclc0lem1  46113  itsclc0lem2  46114  itschlc0yqe  46117  itsclc0xyqsolr  46126