Theorem simp3r 1198

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp13r  1285  simp23r  1291  simp33r  1297  f1oiso2  7105  tfisi  7573  tfrlem5  8016  omeulem1  8208  omeulem2  8209  elfiun  8894  isfin2-2  9741  addid2  10823  mulcan  11277  mulcan2  11278  divass  11316  divdir  11323  div11  11326  ltdiv1  11504  ltmuldiv  11513  lediv2  11530  xaddass2  12644  xlt2add  12654  expaddz  13474  expmulz  13476  resqrex  14610  resqrtcl  14613  o1add  14970  o1mul  14971  o1sub  14972  dvdsgcd  15892  rpexp12i  16066  pythagtriplem4  16156  pythagtriplem11  16162  pythagtriplem13  16164  pcpremul  16180  pceu  16183  pcqmul  16190  pcqdiv  16194  f1ocpbllem  16797  funcoppc  17145  funcres  17166  catcisolem  17366  1stfcl  17447  2ndfcl  17448  prfcl  17453  evlfcl  17472  curf1cl  17478  curfcl  17482  hofcl  17509  latjlej12  17677  latmlem12  17693  latj4  17711  latj4rot  17712  symgsssg  18595  symgfisg  18596  odcong  18677  cmn4  18926  ablsub4  18933  abladdsub4  18934  lsm4  18980  abvdom  19609  abvtrivd  19611  lspsolvlem  19914  lbsextlem2  19931  lidlsubcl  19989  frlmbas3  20920  matinvgcell  21044  matmulcell  21054  ma1repveval  21180  mdetunilem3  21223  mdetuni0  21230  mdetmul  21232  hausflimlem  22587  psmetlecl  22925  xmetlecl  22956  prdsxmetlem  22978  xblcntrps  23020  xblcntr  23021  bndth  23562  cph2ass  23817  iscau3  23881  dvres2  24510  coemullem  24840  vieta1  24901  aalioulem4  24924  cxpcn3lem  25328  angcan  25380  divsqrtsumlem  25557  dchrmusumlema  26069  dchrvmasumlema  26076  dchrisum0lema  26090  logdivsum  26109  padicabv  26206  ax5seglem3  26717  ax5seglem6  26720  axpasch  26727  axeuclid  26749  axcontlem4  26753  axcontlem8  26757  trlsonistrl  27490  pthonispth  27527  spthonisspth  27531  wspthneq1eq2  27638  frgr2wwlkeqm  28110  adjlnop  29863  xreceu  30598  orngmul  30876  rhmdvd  30894  measvunilem  31471  measvuni  31473  bnj1128  32262  umgr2cycl  32388  satfv1fvfmla1  32670  cgrcomim  33450  cgrcoml  33457  cgrcomr  33458  cgrdegen  33465  segconeu  33472  btwnintr  33480  btwnexch3  33481  btwnouttr2  33483  btwnouttr  33485  btwnexch  33486  ifscgr  33505  lineext  33537  linecgr  33542  lineid  33544  idinside  33545  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem14  33561  btwnconn2  33563  btwnconn3  33564  midofsegid  33565  btwnoutside  33586  outsideoftr  33590  lineunray  33608  lineelsb2  33609  itg2addnclem  34958  cnres2  35056  heibor  35114  lsmcv2  36180  lcvat  36181  lcvexchlem4  36188  lcvexchlem5  36189  lfladd  36217  lflsub  36218  lflmul  36219  lshpkrlem4  36264  latm4  36384  omlmod1i2N  36411  cvlsupr7  36499  cvlsupr8  36500  hlatj4  36525  hlrelat3  36563  cvrval3  36564  atcvrj1  36582  atlelt  36589  2atlt  36590  2atjm  36596  3noncolr2  36600  athgt  36607  3dimlem2  36610  3dimlem4OLDN  36616  1cvratex  36624  ps-1  36628  ps-2  36629  hlatexch3N  36631  llnle  36669  atcvrlln2  36670  atcvrlln  36671  lplni2  36688  lplnle  36691  lplnnle2at  36692  lplnnlelln  36694  llncvrlpln2  36708  2llnmeqat  36722  lvolnle3at  36733  lvolnlelln  36735  4atlem0ae  36745  lneq2at  36929  lnjatN  36931  lncvrat  36933  2lnat  36935  elpaddri  36953  paddasslem2  36972  padd4N  36991  hlmod1i  37007  llnexchb2  37020  dalawlem2  37023  pclfinN  37051  pexmidlem4N  37124  pl42lem1N  37130  lhp2lt  37152  lhpexle1  37159  lhpexle2lem  37160  lhpj1  37173  lhpmcvr5N  37178  lhp2at0  37183  lhp2at0nle  37186  lhple  37193  lhpat  37194  lhpat4N  37195  4atexlemnslpq  37207  4atexlem7  37226  ltrn11  37277  ltrnle  37280  ltrnm  37282  ltrnj  37283  ltrncvr  37284  ltrnel  37290  ltrncnvel  37293  ltrncnv  37297  trlat  37320  trl0  37321  trlnidat  37324  trlnid  37330  ltrnatlw  37334  trlne  37336  trlval4  37339  cdlemc5  37346  cdlemd2  37350  cdlemd7  37355  cdlemd8  37356  cdlemd9  37357  cdleme0c  37364  cdleme0e  37368  cdleme0fN  37369  cdleme3g  37385  cdleme3h  37386  cdleme5  37391  cdleme11c  37412  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme0nex  37441  cdleme18a  37442  cdleme22gb  37445  cdleme20zN  37452  cdleme20c  37462  cdleme20k  37470  cdleme21a  37476  cdleme21b  37477  cdleme21c  37478  cdleme21ct  37480  cdleme21h  37485  cdleme22d  37494  cdleme22f  37497  cdleme26ee  37511  cdleme30a  37529  cdlemefs45eN  37582  cdleme36a  37611  cdleme36m  37612  cdleme39a  37616  cdleme42b  37629  cdleme43dN  37643  cdlemeg47rv2  37661  cdlemeg46sfg  37671  cdlemeg46rjgN  37673  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemeg46gfv  37681  cdleme48d  37686  cdleme50ltrn  37708  cdlemf1  37712  cdlemf  37714  cdlemg2dN  37741  cdlemg2fvlem  37745  cdlemg2l  37754  cdlemg7fvbwN  37758  cdlemg7aN  37776  cdlemg10c  37790  cdlemg17a  37812  cdlemg17dALTN  37815  cdlemg18a  37829  cdlemg18b  37830  cdlemg31b0a  37846  cdlemg31a  37848  cdlemg31b  37849  ltrnco  37870  cdlemg48  37888  tgrpov  37899  tendoco2  37919  tendoplco2  37930  cdlemh1  37966  cdlemk1  37982  cdlemk26b-3  38056  cdlemk27-3  38058  cdlemk28-3  38059  cdlemk34  38061  cdlemkfid1N  38072  cdlemkid3N  38084  cdlemkid4  38085  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk51  38104  tendospcanN  38174  cdlemm10N  38269  dicvaddcl  38341  dicvscacl  38342  cdlemn6  38353  dihvalcq2  38398  dihord6b  38411  dihord5apre  38413  dihglbcpreN  38451  dihjatc1  38462  dihmeetlem20N  38477  dih1dimatlem0  38479  dihglblem6  38491  dochexmidlem4  38614  mapdpglem32  38856  mapdh8ad  38930  mapdh9aOLDN  38941  hdmap11lem2  38993  hdmap14lem6  39024  frlmfzowrdb  39163  mzpmfp  39364  mzpsubst  39365  pellex  39452  pellfundex  39503  pellfund14gap  39504  qirropth  39525  rmxypos  39564  congmul  39584  congsub  39587  mzpcong  39589  coprmdvdsb  39602  jm2.15nn0  39620  jm2.16nn0  39621  rpnnen3lem  39648  idomsubgmo  39818  relexp01min  40078  mullimc  41917  islptre  41920  mullimcf  41924  addlimc  41949  0ellimcdiv  41950  limsupre3lem  42033  limsupre3uzlem  42036  fourierdlem48  42459  fourierdlem80  42491  opnvonmbllem2  42935  ovolval5lem3  42956  ovnovollem3  42960  lincfsuppcl  44488  lindslinindimp2lem3  44535  itsclc0lem1  44763  itsclc0lem2  44764  itschlc0yqe  44767  itsclc0xyqsolr  44776