Theorem simp3r 1219

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp13r  1306  simp23r  1312  simp33r  1318  f1oiso2  7340  tfisi  7843  tfrlem5  8354  omeulem1  8555  omeulem2  8556  elfiun  9378  isfin2-2  10291  addlid  11381  mulcan  11839  mulcan2  11840  divass  11878  divdir  11885  ltdiv1  12067  ltmuldiv  12076  lediv2  12093  xaddass2  13264  xlt2add  13274  expaddz  14130  expmulz  14132  resqrex  15289  resqrtcl  15292  o1add  15653  o1mul  15654  o1sub  15655  dvdsgcd  16590  rpexp12i  16771  pythagtriplem4  16867  pythagtriplem11  16873  pythagtriplem13  16875  pcpremul  16891  pceu  16894  pcqmul  16901  pcqdiv  16905  f1ocpbllem  17566  funcoppc  17920  funcres  17941  catcisolem  18155  1stfcl  18241  2ndfcl  18242  prfcl  18247  evlfcl  18266  curf1cl  18272  curfcl  18276  hofcl  18303  latjlej12  18499  latmlem12  18515  latj4  18533  latj4rot  18534  symgsssg  19525  symgfisg  19526  odcong  19607  cmn4  19859  ablsub4  19868  abladdsub4  19869  lsm4  19918  abvdom  20899  abvtrivd  20901  orngmul  20934  lspsolvlem  21232  lbsextlem2  21249  lidlsubcl  21315  frlmbas3  21883  matinvgcell  22549  matmulcell  22559  ma1repveval  22685  mdetunilem3  22728  mdetuni0  22735  mdetmul  22737  hausflimlem  24093  psmetlecl  24429  xmetlecl  24460  prdsxmetlem  24482  xblcntrps  24524  xblcntr  24525  bndth  25074  cph2ass  25329  iscau3  25394  dvres2  26028  coemullem  26364  vieta1  26430  aalioulem4  26453  cxpcn3lem  26866  angcan  26921  divsqrtsumlem  27098  dchrmusumlema  27611  dchrvmasumlema  27618  dchrisum0lema  27632  logdivsum  27651  padicabv  27748  cofcut1  28067  cofcut2  28069  divmulsw  28340  precsexlem8  28361  precsexlem9  28362  bdayfinbndlem1  28614  ax5seglem3  29186  ax5seglem6  29189  axpasch  29196  axeuclid  29218  axcontlem4  29222  axcontlem8  29226  trlsonistrl  29961  pthonispth  30000  spthonisspth  30004  wspthneq1eq2  30114  frgr2wwlkeqm  30587  adjlnop  32343  xreceu  33149  rhmdvd  33554  measvunilem  34514  measvuni  34516  bnj1128  35290  umgr2cycl  35499  satfv1fvfmla1  35781  cgrcomim  36347  cgrcoml  36354  cgrcomr  36355  cgrdegen  36362  segconeu  36369  btwnintr  36377  btwnexch3  36378  btwnouttr2  36380  btwnouttr  36382  btwnexch  36383  ifscgr  36402  lineext  36434  linecgr  36439  lineid  36441  idinside  36442  btwnconn1lem3  36447  btwnconn1lem4  36448  btwnconn1lem14  36458  btwnconn2  36460  btwnconn3  36461  midofsegid  36462  btwnoutside  36483  outsideoftr  36487  lineunray  36505  lineelsb2  36506  itg2addnclem  38177  cnres2  38269  heibor  38327  lsmcv2  39660  lcvat  39661  lcvexchlem4  39668  lcvexchlem5  39669  lfladd  39697  lflsub  39698  lflmul  39699  lshpkrlem4  39744  latm4  39864  omlmod1i2N  39891  cvlsupr7  39979  cvlsupr8  39980  hlatj4  40005  hlrelat3  40043  cvrval3  40044  atcvrj1  40062  atlelt  40069  2atlt  40070  2atjm  40076  3noncolr2  40080  athgt  40087  3dimlem2  40090  3dimlem4OLDN  40096  1cvratex  40104  ps-1  40108  ps-2  40109  hlatexch3N  40111  llnle  40149  atcvrlln2  40150  atcvrlln  40151  lplni2  40168  lplnle  40171  lplnnle2at  40172  lplnnlelln  40174  llncvrlpln2  40188  2llnmeqat  40202  lvolnle3at  40213  lvolnlelln  40215  4atlem0ae  40225  lneq2at  40409  lnjatN  40411  lncvrat  40413  2lnat  40415  elpaddri  40433  paddasslem2  40452  padd4N  40471  hlmod1i  40487  llnexchb2  40500  dalawlem2  40503  pclfinN  40531  pexmidlem4N  40604  pl42lem1N  40610  lhp2lt  40632  lhpexle1  40639  lhpexle2lem  40640  lhpj1  40653  lhpmcvr5N  40658  lhp2at0  40663  lhp2at0nle  40666  lhple  40673  lhpat  40674  lhpat4N  40675  4atexlemnslpq  40687  4atexlem7  40706  ltrn11  40757  ltrnle  40760  ltrnm  40762  ltrnj  40763  ltrncvr  40764  ltrnel  40770  ltrncnvel  40773  ltrncnv  40777  trlat  40800  trl0  40801  trlnidat  40804  trlnid  40810  ltrnatlw  40814  trlne  40816  trlval4  40819  cdlemc5  40826  cdlemd2  40830  cdlemd7  40835  cdlemd8  40836  cdlemd9  40837  cdleme0c  40844  cdleme0e  40848  cdleme0fN  40849  cdleme3g  40865  cdleme3h  40866  cdleme5  40871  cdleme11c  40892  cdleme11h  40897  cdleme11j  40898  cdleme11k  40899  cdleme0nex  40921  cdleme18a  40922  cdleme22gb  40925  cdleme20zN  40932  cdleme20c  40942  cdleme20k  40950  cdleme21a  40956  cdleme21b  40957  cdleme21c  40958  cdleme21ct  40960  cdleme21h  40965  cdleme22d  40974  cdleme22f  40977  cdleme26ee  40991  cdleme30a  41009  cdlemefs45eN  41062  cdleme36a  41091  cdleme36m  41092  cdleme39a  41096  cdleme42b  41109  cdleme43dN  41123  cdlemeg47rv2  41141  cdlemeg46sfg  41151  cdlemeg46rjgN  41153  cdlemeg46rgv  41159  cdlemeg46req  41160  cdlemeg46gfv  41161  cdleme48d  41166  cdleme50ltrn  41188  cdlemf1  41192  cdlemf  41194  cdlemg2dN  41221  cdlemg2fvlem  41225  cdlemg2l  41234  cdlemg7fvbwN  41238  cdlemg7aN  41256  cdlemg10c  41270  cdlemg17a  41292  cdlemg17dALTN  41295  cdlemg18a  41309  cdlemg18b  41310  cdlemg31b0a  41326  cdlemg31a  41328  cdlemg31b  41329  ltrnco  41350  cdlemg48  41368  tgrpov  41379  tendoco2  41399  tendoplco2  41410  cdlemh1  41446  cdlemk1  41462  cdlemk26b-3  41536  cdlemk27-3  41538  cdlemk28-3  41539  cdlemk34  41541  cdlemkfid1N  41552  cdlemkid3N  41564  cdlemkid4  41565  cdlemk35s-id  41569  cdlemk39s-id  41571  cdlemk51  41584  tendospcanN  41654  cdlemm10N  41749  dicvaddcl  41821  dicvscacl  41822  cdlemn6  41833  dihvalcq2  41878  dihord6b  41891  dihord5apre  41893  dihglbcpreN  41931  dihjatc1  41942  dihmeetlem20N  41957  dih1dimatlem0  41959  dihglblem6  41971  dochexmidlem4  42094  mapdpglem32  42336  mapdh8ad  42410  mapdh9aOLDN  42421  hdmap11lem2  42473  hdmap14lem6  42504  frlmfzowrdb  43133  mzpmfp  43335  mzpsubst  43336  pellex  43419  pellfundex  43470  pellfund14gap  43471  qirropth  43492  rmxypos  43531  congmul  43551  congsub  43554  mzpcong  43556  coprmdvdsb  43569  jm2.15nn0  43587  jm2.16nn0  43588  rpnnen3lem  43615  idomsubgmo  43777  relexp01min  44296  mullimc  46191  islptre  46194  mullimcf  46198  addlimc  46221  0ellimcdiv  46222  limsupre3lem  46305  limsupre3uzlem  46308  fourierdlem48  46727  fourierdlem80  46759  opnvonmbllem2  47206  ovolval5lem3  47227  ovnovollem3  47231  difltmodne  47941  isubgr3stgrlem1  48587  grlimedgclnbgr  48616  mapprop  48978  lincfsuppcl  49045  lindslinindimp2lem3  49092  itsclc0lem1  49388  itsclc0lem2  49389  itschlc0yqe  49392  itsclc0xyqsolr  49401  swapffunc  49912  fucofunc  49989  fucoppc  50040