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 1087

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 1089

This theorem is referenced by:  simp13r  1289  simp23r  1295  simp33r  1301  f1oiso2  7388  tfisi  7896  tfrlem5  8436  omeulem1  8638  omeulem2  8639  elfiun  9499  isfin2-2  10388  addlid  11473  mulcan  11927  mulcan2  11928  divass  11967  divdir  11974  div11OLD  11978  ltdiv1  12159  ltmuldiv  12168  lediv2  12185  xaddass2  13312  xlt2add  13322  expaddz  14157  expmulz  14159  resqrex  15299  resqrtcl  15302  o1add  15660  o1mul  15661  o1sub  15662  dvdsgcd  16591  rpexp12i  16771  pythagtriplem4  16866  pythagtriplem11  16872  pythagtriplem13  16874  pcpremul  16890  pceu  16893  pcqmul  16900  pcqdiv  16904  f1ocpbllem  17584  funcoppc  17939  funcres  17960  catcisolem  18177  1stfcl  18266  2ndfcl  18267  prfcl  18272  evlfcl  18292  curf1cl  18298  curfcl  18302  hofcl  18329  latjlej12  18525  latmlem12  18541  latj4  18559  latj4rot  18560  symgsssg  19509  symgfisg  19510  odcong  19591  cmn4  19843  ablsub4  19852  abladdsub4  19853  lsm4  19902  abvdom  20853  abvtrivd  20855  lspsolvlem  21167  lbsextlem2  21184  lidlsubcl  21257  frlmbas3  21819  matinvgcell  22462  matmulcell  22472  ma1repveval  22598  mdetunilem3  22641  mdetuni0  22648  mdetmul  22650  hausflimlem  24008  psmetlecl  24346  xmetlecl  24377  prdsxmetlem  24399  xblcntrps  24441  xblcntr  24442  bndth  25009  cph2ass  25266  iscau3  25331  dvres2  25967  coemullem  26309  vieta1  26372  aalioulem4  26395  cxpcn3lem  26808  angcan  26863  divsqrtsumlem  27041  dchrmusumlema  27555  dchrvmasumlema  27562  dchrisum0lema  27576  logdivsum  27595  padicabv  27692  cofcut1  27972  cofcut2  27974  divsmulw  28236  precsexlem8  28256  precsexlem9  28257  ax5seglem3  28964  ax5seglem6  28967  axpasch  28974  axeuclid  28996  axcontlem4  29000  axcontlem8  29004  trlsonistrl  29745  pthonispth  29782  spthonisspth  29786  wspthneq1eq2  29893  frgr2wwlkeqm  30363  adjlnop  32118  xreceu  32886  orngmul  33298  rhmdvd  33313  measvunilem  34176  measvuni  34178  bnj1128  34966  umgr2cycl  35109  satfv1fvfmla1  35391  cgrcomim  35953  cgrcoml  35960  cgrcomr  35961  cgrdegen  35968  segconeu  35975  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  btwnouttr  35988  btwnexch  35989  ifscgr  36008  lineext  36040  linecgr  36045  lineid  36047  idinside  36048  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem14  36064  btwnconn2  36066  btwnconn3  36067  midofsegid  36068  btwnoutside  36089  outsideoftr  36093  lineunray  36111  lineelsb2  36112  itg2addnclem  37631  cnres2  37723  heibor  37781  lsmcv2  38985  lcvat  38986  lcvexchlem4  38993  lcvexchlem5  38994  lfladd  39022  lflsub  39023  lflmul  39024  lshpkrlem4  39069  latm4  39189  omlmod1i2N  39216  cvlsupr7  39304  cvlsupr8  39305  hlatj4  39330  hlrelat3  39369  cvrval3  39370  atcvrj1  39388  atlelt  39395  2atlt  39396  2atjm  39402  3noncolr2  39406  athgt  39413  3dimlem2  39416  3dimlem4OLDN  39422  1cvratex  39430  ps-1  39434  ps-2  39435  hlatexch3N  39437  llnle  39475  atcvrlln2  39476  atcvrlln  39477  lplni2  39494  lplnle  39497  lplnnle2at  39498  lplnnlelln  39500  llncvrlpln2  39514  2llnmeqat  39528  lvolnle3at  39539  lvolnlelln  39541  4atlem0ae  39551  lneq2at  39735  lnjatN  39737  lncvrat  39739  2lnat  39741  elpaddri  39759  paddasslem2  39778  padd4N  39797  hlmod1i  39813  llnexchb2  39826  dalawlem2  39829  pclfinN  39857  pexmidlem4N  39930  pl42lem1N  39936  lhp2lt  39958  lhpexle1  39965  lhpexle2lem  39966  lhpj1  39979  lhpmcvr5N  39984  lhp2at0  39989  lhp2at0nle  39992  lhple  39999  lhpat  40000  lhpat4N  40001  4atexlemnslpq  40013  4atexlem7  40032  ltrn11  40083  ltrnle  40086  ltrnm  40088  ltrnj  40089  ltrncvr  40090  ltrnel  40096  ltrncnvel  40099  ltrncnv  40103  trlat  40126  trl0  40127  trlnidat  40130  trlnid  40136  ltrnatlw  40140  trlne  40142  trlval4  40145  cdlemc5  40152  cdlemd2  40156  cdlemd7  40161  cdlemd8  40162  cdlemd9  40163  cdleme0c  40170  cdleme0e  40174  cdleme0fN  40175  cdleme3g  40191  cdleme3h  40192  cdleme5  40197  cdleme11c  40218  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme0nex  40247  cdleme18a  40248  cdleme22gb  40251  cdleme20zN  40258  cdleme20c  40268  cdleme20k  40276  cdleme21a  40282  cdleme21b  40283  cdleme21c  40284  cdleme21ct  40286  cdleme21h  40291  cdleme22d  40300  cdleme22f  40303  cdleme26ee  40317  cdleme30a  40335  cdlemefs45eN  40388  cdleme36a  40417  cdleme36m  40418  cdleme39a  40422  cdleme42b  40435  cdleme43dN  40449  cdlemeg47rv2  40467  cdlemeg46sfg  40477  cdlemeg46rjgN  40479  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemeg46gfv  40487  cdleme48d  40492  cdleme50ltrn  40514  cdlemf1  40518  cdlemf  40520  cdlemg2dN  40547  cdlemg2fvlem  40551  cdlemg2l  40560  cdlemg7fvbwN  40564  cdlemg7aN  40582  cdlemg10c  40596  cdlemg17a  40618  cdlemg17dALTN  40621  cdlemg18a  40635  cdlemg18b  40636  cdlemg31b0a  40652  cdlemg31a  40654  cdlemg31b  40655  ltrnco  40676  cdlemg48  40694  tgrpov  40705  tendoco2  40725  tendoplco2  40736  cdlemh1  40772  cdlemk1  40788  cdlemk26b-3  40862  cdlemk27-3  40864  cdlemk28-3  40865  cdlemk34  40867  cdlemkfid1N  40878  cdlemkid3N  40890  cdlemkid4  40891  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk51  40910  tendospcanN  40980  cdlemm10N  41075  dicvaddcl  41147  dicvscacl  41148  cdlemn6  41159  dihvalcq2  41204  dihord6b  41217  dihord5apre  41219  dihglbcpreN  41257  dihjatc1  41268  dihmeetlem20N  41283  dih1dimatlem0  41285  dihglblem6  41297  dochexmidlem4  41420  mapdpglem32  41662  mapdh8ad  41736  mapdh9aOLDN  41747  hdmap11lem2  41799  hdmap14lem6  41830  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  43154  relexp01min  43675  mullimc  45537  islptre  45540  mullimcf  45544  addlimc  45569  0ellimcdiv  45570  limsupre3lem  45653  limsupre3uzlem  45656  fourierdlem48  46075  fourierdlem80  46107  opnvonmbllem2  46554  ovolval5lem3  46575  ovnovollem3  46579  mapprop  48071  lincfsuppcl  48142  lindslinindimp2lem3  48189  itsclc0lem1  48490  itsclc0lem2  48491  itschlc0yqe  48494  itsclc0xyqsolr  48503