Theorem simp3r 1202

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  1289  simp23r  1295  simp33r  1301  f1oiso2  7355  tfisi  7863  tfrlem5  8403  omeulem1  8603  omeulem2  8604  elfiun  9453  isfin2-2  10342  addlid  11427  mulcan  11883  mulcan2  11884  divass  11923  divdir  11930  div11OLD  11934  ltdiv1  12115  ltmuldiv  12124  lediv2  12141  xaddass2  13275  xlt2add  13285  expaddz  14130  expmulz  14132  resqrex  15272  resqrtcl  15275  o1add  15633  o1mul  15634  o1sub  15635  dvdsgcd  16564  rpexp12i  16744  pythagtriplem4  16840  pythagtriplem11  16846  pythagtriplem13  16848  pcpremul  16864  pceu  16867  pcqmul  16874  pcqdiv  16878  f1ocpbllem  17545  funcoppc  17896  funcres  17917  catcisolem  18131  1stfcl  18217  2ndfcl  18218  prfcl  18223  evlfcl  18242  curf1cl  18248  curfcl  18252  hofcl  18279  latjlej12  18474  latmlem12  18490  latj4  18508  latj4rot  18509  symgsssg  19458  symgfisg  19459  odcong  19540  cmn4  19792  ablsub4  19801  abladdsub4  19802  lsm4  19851  abvdom  20804  abvtrivd  20806  lspsolvlem  21117  lbsextlem2  21134  lidlsubcl  21201  frlmbas3  21763  matinvgcell  22408  matmulcell  22418  ma1repveval  22544  mdetunilem3  22587  mdetuni0  22594  mdetmul  22596  hausflimlem  23952  psmetlecl  24289  xmetlecl  24320  prdsxmetlem  24342  xblcntrps  24384  xblcntr  24385  bndth  24945  cph2ass  25202  iscau3  25267  dvres2  25902  coemullem  26244  vieta1  26309  aalioulem4  26332  cxpcn3lem  26745  angcan  26800  divsqrtsumlem  26978  dchrmusumlema  27492  dchrvmasumlema  27499  dchrisum0lema  27513  logdivsum  27532  padicabv  27629  cofcut1  27909  cofcut2  27911  divsmulw  28173  precsexlem8  28193  precsexlem9  28194  ax5seglem3  28895  ax5seglem6  28898  axpasch  28905  axeuclid  28927  axcontlem4  28931  axcontlem8  28935  trlsonistrl  29674  pthonispth  29713  spthonisspth  29717  wspthneq1eq2  29827  frgr2wwlkeqm  30297  adjlnop  32052  xreceu  32851  orngmul  33279  rhmdvd  33294  measvunilem  34154  measvuni  34156  bnj1128  34945  umgr2cycl  35087  satfv1fvfmla1  35369  cgrcomim  35931  cgrcoml  35938  cgrcomr  35939  cgrdegen  35946  segconeu  35953  btwnintr  35961  btwnexch3  35962  btwnouttr2  35964  btwnouttr  35966  btwnexch  35967  ifscgr  35986  lineext  36018  linecgr  36023  lineid  36025  idinside  36026  btwnconn1lem3  36031  btwnconn1lem4  36032  btwnconn1lem14  36042  btwnconn2  36044  btwnconn3  36045  midofsegid  36046  btwnoutside  36067  outsideoftr  36071  lineunray  36089  lineelsb2  36090  itg2addnclem  37619  cnres2  37711  heibor  37769  lsmcv2  38971  lcvat  38972  lcvexchlem4  38979  lcvexchlem5  38980  lfladd  39008  lflsub  39009  lflmul  39010  lshpkrlem4  39055  latm4  39175  omlmod1i2N  39202  cvlsupr7  39290  cvlsupr8  39291  hlatj4  39316  hlrelat3  39355  cvrval3  39356  atcvrj1  39374  atlelt  39381  2atlt  39382  2atjm  39388  3noncolr2  39392  athgt  39399  3dimlem2  39402  3dimlem4OLDN  39408  1cvratex  39416  ps-1  39420  ps-2  39421  hlatexch3N  39423  llnle  39461  atcvrlln2  39462  atcvrlln  39463  lplni2  39480  lplnle  39483  lplnnle2at  39484  lplnnlelln  39486  llncvrlpln2  39500  2llnmeqat  39514  lvolnle3at  39525  lvolnlelln  39527  4atlem0ae  39537  lneq2at  39721  lnjatN  39723  lncvrat  39725  2lnat  39727  elpaddri  39745  paddasslem2  39764  padd4N  39783  hlmod1i  39799  llnexchb2  39812  dalawlem2  39815  pclfinN  39843  pexmidlem4N  39916  pl42lem1N  39922  lhp2lt  39944  lhpexle1  39951  lhpexle2lem  39952  lhpj1  39965  lhpmcvr5N  39970  lhp2at0  39975  lhp2at0nle  39978  lhple  39985  lhpat  39986  lhpat4N  39987  4atexlemnslpq  39999  4atexlem7  40018  ltrn11  40069  ltrnle  40072  ltrnm  40074  ltrnj  40075  ltrncvr  40076  ltrnel  40082  ltrncnvel  40085  ltrncnv  40089  trlat  40112  trl0  40113  trlnidat  40116  trlnid  40122  ltrnatlw  40126  trlne  40128  trlval4  40131  cdlemc5  40138  cdlemd2  40142  cdlemd7  40147  cdlemd8  40148  cdlemd9  40149  cdleme0c  40156  cdleme0e  40160  cdleme0fN  40161  cdleme3g  40177  cdleme3h  40178  cdleme5  40183  cdleme11c  40204  cdleme11h  40209  cdleme11j  40210  cdleme11k  40211  cdleme0nex  40233  cdleme18a  40234  cdleme22gb  40237  cdleme20zN  40244  cdleme20c  40254  cdleme20k  40262  cdleme21a  40268  cdleme21b  40269  cdleme21c  40270  cdleme21ct  40272  cdleme21h  40277  cdleme22d  40286  cdleme22f  40289  cdleme26ee  40303  cdleme30a  40321  cdlemefs45eN  40374  cdleme36a  40403  cdleme36m  40404  cdleme39a  40408  cdleme42b  40421  cdleme43dN  40435  cdlemeg47rv2  40453  cdlemeg46sfg  40463  cdlemeg46rjgN  40465  cdlemeg46rgv  40471  cdlemeg46req  40472  cdlemeg46gfv  40473  cdleme48d  40478  cdleme50ltrn  40500  cdlemf1  40504  cdlemf  40506  cdlemg2dN  40533  cdlemg2fvlem  40537  cdlemg2l  40546  cdlemg7fvbwN  40550  cdlemg7aN  40568  cdlemg10c  40582  cdlemg17a  40604  cdlemg17dALTN  40607  cdlemg18a  40621  cdlemg18b  40622  cdlemg31b0a  40638  cdlemg31a  40640  cdlemg31b  40641  ltrnco  40662  cdlemg48  40680  tgrpov  40691  tendoco2  40711  tendoplco2  40722  cdlemh1  40758  cdlemk1  40774  cdlemk26b-3  40848  cdlemk27-3  40850  cdlemk28-3  40851  cdlemk34  40853  cdlemkfid1N  40864  cdlemkid3N  40876  cdlemkid4  40877  cdlemk35s-id  40881  cdlemk39s-id  40883  cdlemk51  40896  tendospcanN  40966  cdlemm10N  41061  dicvaddcl  41133  dicvscacl  41134  cdlemn6  41145  dihvalcq2  41190  dihord6b  41203  dihord5apre  41205  dihglbcpreN  41243  dihjatc1  41254  dihmeetlem20N  41269  dih1dimatlem0  41271  dihglblem6  41283  dochexmidlem4  41406  mapdpglem32  41648  mapdh8ad  41722  mapdh9aOLDN  41733  hdmap11lem2  41785  hdmap14lem6  41816  frlmfzowrdb  42459  mzpmfp  42703  mzpsubst  42704  pellex  42791  pellfundex  42842  pellfund14gap  42843  qirropth  42864  rmxypos  42904  congmul  42924  congsub  42927  mzpcong  42929  coprmdvdsb  42942  jm2.15nn0  42960  jm2.16nn0  42961  rpnnen3lem  42988  idomsubgmo  43150  relexp01min  43671  mullimc  45576  islptre  45579  mullimcf  45583  addlimc  45608  0ellimcdiv  45609  limsupre3lem  45692  limsupre3uzlem  45695  fourierdlem48  46114  fourierdlem80  46146  opnvonmbllem2  46593  ovolval5lem3  46614  ovnovollem3  46618  difltmodne  47290  isubgr3stgrlem1  47879  mapprop  48208  lincfsuppcl  48276  lindslinindimp2lem3  48323  itsclc0lem1  48623  itsclc0lem2  48624  itschlc0yqe  48627  itsclc0xyqsolr  48636  swapffunc  48947  fucofunc  49018