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  7350  tfisi  7859  tfrlem5  8399  omeulem1  8599  omeulem2  8600  elfiun  9447  isfin2-2  10338  addlid  11423  mulcan  11879  mulcan2  11880  divass  11919  divdir  11926  div11OLD  11930  ltdiv1  12111  ltmuldiv  12120  lediv2  12137  xaddass2  13271  xlt2add  13281  expaddz  14129  expmulz  14131  resqrex  15274  resqrtcl  15277  o1add  15635  o1mul  15636  o1sub  15637  dvdsgcd  16568  rpexp12i  16748  pythagtriplem4  16844  pythagtriplem11  16850  pythagtriplem13  16852  pcpremul  16868  pceu  16871  pcqmul  16878  pcqdiv  16882  f1ocpbllem  17543  funcoppc  17893  funcres  17914  catcisolem  18128  1stfcl  18214  2ndfcl  18215  prfcl  18220  evlfcl  18239  curf1cl  18245  curfcl  18249  hofcl  18276  latjlej12  18470  latmlem12  18486  latj4  18504  latj4rot  18505  symgsssg  19453  symgfisg  19454  odcong  19535  cmn4  19787  ablsub4  19796  abladdsub4  19797  lsm4  19846  abvdom  20795  abvtrivd  20797  lspsolvlem  21108  lbsextlem2  21125  lidlsubcl  21190  frlmbas3  21741  matinvgcell  22378  matmulcell  22388  ma1repveval  22514  mdetunilem3  22557  mdetuni0  22564  mdetmul  22566  hausflimlem  23922  psmetlecl  24259  xmetlecl  24290  prdsxmetlem  24312  xblcntrps  24354  xblcntr  24355  bndth  24913  cph2ass  25170  iscau3  25235  dvres2  25870  coemullem  26212  vieta1  26277  aalioulem4  26300  cxpcn3lem  26714  angcan  26769  divsqrtsumlem  26947  dchrmusumlema  27461  dchrvmasumlema  27468  dchrisum0lema  27482  logdivsum  27501  padicabv  27598  cofcut1  27885  cofcut2  27887  divsmulw  28153  precsexlem8  28173  precsexlem9  28174  ax5seglem3  28915  ax5seglem6  28918  axpasch  28925  axeuclid  28947  axcontlem4  28951  axcontlem8  28955  trlsonistrl  29694  pthonispth  29733  spthonisspth  29737  wspthneq1eq2  29847  frgr2wwlkeqm  30317  adjlnop  32072  xreceu  32901  orngmul  33330  rhmdvd  33345  measvunilem  34248  measvuni  34250  bnj1128  35026  umgr2cycl  35168  satfv1fvfmla1  35450  cgrcomim  36012  cgrcoml  36019  cgrcomr  36020  cgrdegen  36027  segconeu  36034  btwnintr  36042  btwnexch3  36043  btwnouttr2  36045  btwnouttr  36047  btwnexch  36048  ifscgr  36067  lineext  36099  linecgr  36104  lineid  36106  idinside  36107  btwnconn1lem3  36112  btwnconn1lem4  36113  btwnconn1lem14  36123  btwnconn2  36125  btwnconn3  36126  midofsegid  36127  btwnoutside  36148  outsideoftr  36152  lineunray  36170  lineelsb2  36171  itg2addnclem  37700  cnres2  37792  heibor  37850  lsmcv2  39052  lcvat  39053  lcvexchlem4  39060  lcvexchlem5  39061  lfladd  39089  lflsub  39090  lflmul  39091  lshpkrlem4  39136  latm4  39256  omlmod1i2N  39283  cvlsupr7  39371  cvlsupr8  39372  hlatj4  39397  hlrelat3  39436  cvrval3  39437  atcvrj1  39455  atlelt  39462  2atlt  39463  2atjm  39469  3noncolr2  39473  athgt  39480  3dimlem2  39483  3dimlem4OLDN  39489  1cvratex  39497  ps-1  39501  ps-2  39502  hlatexch3N  39504  llnle  39542  atcvrlln2  39543  atcvrlln  39544  lplni2  39561  lplnle  39564  lplnnle2at  39565  lplnnlelln  39567  llncvrlpln2  39581  2llnmeqat  39595  lvolnle3at  39606  lvolnlelln  39608  4atlem0ae  39618  lneq2at  39802  lnjatN  39804  lncvrat  39806  2lnat  39808  elpaddri  39826  paddasslem2  39845  padd4N  39864  hlmod1i  39880  llnexchb2  39893  dalawlem2  39896  pclfinN  39924  pexmidlem4N  39997  pl42lem1N  40003  lhp2lt  40025  lhpexle1  40032  lhpexle2lem  40033  lhpj1  40046  lhpmcvr5N  40051  lhp2at0  40056  lhp2at0nle  40059  lhple  40066  lhpat  40067  lhpat4N  40068  4atexlemnslpq  40080  4atexlem7  40099  ltrn11  40150  ltrnle  40153  ltrnm  40155  ltrnj  40156  ltrncvr  40157  ltrnel  40163  ltrncnvel  40166  ltrncnv  40170  trlat  40193  trl0  40194  trlnidat  40197  trlnid  40203  ltrnatlw  40207  trlne  40209  trlval4  40212  cdlemc5  40219  cdlemd2  40223  cdlemd7  40228  cdlemd8  40229  cdlemd9  40230  cdleme0c  40237  cdleme0e  40241  cdleme0fN  40242  cdleme3g  40258  cdleme3h  40259  cdleme5  40264  cdleme11c  40285  cdleme11h  40290  cdleme11j  40291  cdleme11k  40292  cdleme0nex  40314  cdleme18a  40315  cdleme22gb  40318  cdleme20zN  40325  cdleme20c  40335  cdleme20k  40343  cdleme21a  40349  cdleme21b  40350  cdleme21c  40351  cdleme21ct  40353  cdleme21h  40358  cdleme22d  40367  cdleme22f  40370  cdleme26ee  40384  cdleme30a  40402  cdlemefs45eN  40455  cdleme36a  40484  cdleme36m  40485  cdleme39a  40489  cdleme42b  40502  cdleme43dN  40516  cdlemeg47rv2  40534  cdlemeg46sfg  40544  cdlemeg46rjgN  40546  cdlemeg46rgv  40552  cdlemeg46req  40553  cdlemeg46gfv  40554  cdleme48d  40559  cdleme50ltrn  40581  cdlemf1  40585  cdlemf  40587  cdlemg2dN  40614  cdlemg2fvlem  40618  cdlemg2l  40627  cdlemg7fvbwN  40631  cdlemg7aN  40649  cdlemg10c  40663  cdlemg17a  40685  cdlemg17dALTN  40688  cdlemg18a  40702  cdlemg18b  40703  cdlemg31b0a  40719  cdlemg31a  40721  cdlemg31b  40722  ltrnco  40743  cdlemg48  40761  tgrpov  40772  tendoco2  40792  tendoplco2  40803  cdlemh1  40839  cdlemk1  40855  cdlemk26b-3  40929  cdlemk27-3  40931  cdlemk28-3  40932  cdlemk34  40934  cdlemkfid1N  40945  cdlemkid3N  40957  cdlemkid4  40958  cdlemk35s-id  40962  cdlemk39s-id  40964  cdlemk51  40977  tendospcanN  41047  cdlemm10N  41142  dicvaddcl  41214  dicvscacl  41215  cdlemn6  41226  dihvalcq2  41271  dihord6b  41284  dihord5apre  41286  dihglbcpreN  41324  dihjatc1  41335  dihmeetlem20N  41350  dih1dimatlem0  41352  dihglblem6  41364  dochexmidlem4  41487  mapdpglem32  41729  mapdh8ad  41803  mapdh9aOLDN  41814  hdmap11lem2  41866  hdmap14lem6  41897  frlmfzowrdb  42502  mzpmfp  42745  mzpsubst  42746  pellex  42833  pellfundex  42884  pellfund14gap  42885  qirropth  42906  rmxypos  42946  congmul  42966  congsub  42969  mzpcong  42971  coprmdvdsb  42984  jm2.15nn0  43002  jm2.16nn0  43003  rpnnen3lem  43030  idomsubgmo  43192  relexp01min  43712  mullimc  45625  islptre  45628  mullimcf  45632  addlimc  45657  0ellimcdiv  45658  limsupre3lem  45741  limsupre3uzlem  45744  fourierdlem48  46163  fourierdlem80  46195  opnvonmbllem2  46642  ovolval5lem3  46663  ovnovollem3  46667  difltmodne  47351  isubgr3stgrlem1  47958  mapprop  48301  lincfsuppcl  48369  lindslinindimp2lem3  48416  itsclc0lem1  48716  itsclc0lem2  48717  itschlc0yqe  48720  itsclc0xyqsolr  48729  swapffunc  49179  fucofunc  49250