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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp13r  1289  simp23r  1295  simp33r  1301  f1oiso2  7351  tfisi  7850  tfrlem5  8382  omeulem1  8584  omeulem2  8585  elfiun  9427  isfin2-2  10316  addlid  11401  mulcan  11855  mulcan2  11856  divass  11894  divdir  11901  div11  11904  ltdiv1  12082  ltmuldiv  12091  lediv2  12108  xaddass2  13233  xlt2add  13243  expaddz  14076  expmulz  14078  resqrex  15201  resqrtcl  15204  o1add  15562  o1mul  15563  o1sub  15564  dvdsgcd  16490  rpexp12i  16665  pythagtriplem4  16756  pythagtriplem11  16762  pythagtriplem13  16764  pcpremul  16780  pceu  16783  pcqmul  16790  pcqdiv  16794  f1ocpbllem  17474  funcoppc  17829  funcres  17850  catcisolem  18064  1stfcl  18153  2ndfcl  18154  prfcl  18159  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  latjlej12  18412  latmlem12  18428  latj4  18446  latj4rot  18447  symgsssg  19376  symgfisg  19377  odcong  19458  cmn4  19710  ablsub4  19719  abladdsub4  19720  lsm4  19769  abvdom  20589  abvtrivd  20591  lspsolvlem  20900  lbsextlem2  20917  lidlsubcl  20988  frlmbas3  21550  matinvgcell  22157  matmulcell  22167  ma1repveval  22293  mdetunilem3  22336  mdetuni0  22343  mdetmul  22345  hausflimlem  23703  psmetlecl  24041  xmetlecl  24072  prdsxmetlem  24094  xblcntrps  24136  xblcntr  24137  bndth  24698  cph2ass  24954  iscau3  25019  dvres2  25653  coemullem  25988  vieta1  26049  aalioulem4  26072  cxpcn3lem  26479  angcan  26531  divsqrtsumlem  26708  dchrmusumlema  27220  dchrvmasumlema  27227  dchrisum0lema  27241  logdivsum  27260  padicabv  27357  cofcut1  27633  cofcut2  27635  divsmulw  27867  precsexlem8  27887  precsexlem9  27888  ax5seglem3  28444  ax5seglem6  28447  axpasch  28454  axeuclid  28476  axcontlem4  28480  axcontlem8  28484  trlsonistrl  29221  pthonispth  29258  spthonisspth  29262  wspthneq1eq2  29369  frgr2wwlkeqm  29839  adjlnop  31594  xreceu  32343  orngmul  32679  rhmdvd  32694  measvunilem  33496  measvuni  33498  bnj1128  34287  umgr2cycl  34418  satfv1fvfmla1  34700  cgrcomim  35253  cgrcoml  35260  cgrcomr  35261  cgrdegen  35268  segconeu  35275  btwnintr  35283  btwnexch3  35284  btwnouttr2  35286  btwnouttr  35288  btwnexch  35289  ifscgr  35308  lineext  35340  linecgr  35345  lineid  35347  idinside  35348  btwnconn1lem3  35353  btwnconn1lem4  35354  btwnconn1lem14  35364  btwnconn2  35366  btwnconn3  35367  midofsegid  35368  btwnoutside  35389  outsideoftr  35393  lineunray  35411  lineelsb2  35412  itg2addnclem  36842  cnres2  36934  heibor  36992  lsmcv2  38202  lcvat  38203  lcvexchlem4  38210  lcvexchlem5  38211  lfladd  38239  lflsub  38240  lflmul  38241  lshpkrlem4  38286  latm4  38406  omlmod1i2N  38433  cvlsupr7  38521  cvlsupr8  38522  hlatj4  38547  hlrelat3  38586  cvrval3  38587  atcvrj1  38605  atlelt  38612  2atlt  38613  2atjm  38619  3noncolr2  38623  athgt  38630  3dimlem2  38633  3dimlem4OLDN  38639  1cvratex  38647  ps-1  38651  ps-2  38652  hlatexch3N  38654  llnle  38692  atcvrlln2  38693  atcvrlln  38694  lplni2  38711  lplnle  38714  lplnnle2at  38715  lplnnlelln  38717  llncvrlpln2  38731  2llnmeqat  38745  lvolnle3at  38756  lvolnlelln  38758  4atlem0ae  38768  lneq2at  38952  lnjatN  38954  lncvrat  38956  2lnat  38958  elpaddri  38976  paddasslem2  38995  padd4N  39014  hlmod1i  39030  llnexchb2  39043  dalawlem2  39046  pclfinN  39074  pexmidlem4N  39147  pl42lem1N  39153  lhp2lt  39175  lhpexle1  39182  lhpexle2lem  39183  lhpj1  39196  lhpmcvr5N  39201  lhp2at0  39206  lhp2at0nle  39209  lhple  39216  lhpat  39217  lhpat4N  39218  4atexlemnslpq  39230  4atexlem7  39249  ltrn11  39300  ltrnle  39303  ltrnm  39305  ltrnj  39306  ltrncvr  39307  ltrnel  39313  ltrncnvel  39316  ltrncnv  39320  trlat  39343  trl0  39344  trlnidat  39347  trlnid  39353  ltrnatlw  39357  trlne  39359  trlval4  39362  cdlemc5  39369  cdlemd2  39373  cdlemd7  39378  cdlemd8  39379  cdlemd9  39380  cdleme0c  39387  cdleme0e  39391  cdleme0fN  39392  cdleme3g  39408  cdleme3h  39409  cdleme5  39414  cdleme11c  39435  cdleme11h  39440  cdleme11j  39441  cdleme11k  39442  cdleme0nex  39464  cdleme18a  39465  cdleme22gb  39468  cdleme20zN  39475  cdleme20c  39485  cdleme20k  39493  cdleme21a  39499  cdleme21b  39500  cdleme21c  39501  cdleme21ct  39503  cdleme21h  39508  cdleme22d  39517  cdleme22f  39520  cdleme26ee  39534  cdleme30a  39552  cdlemefs45eN  39605  cdleme36a  39634  cdleme36m  39635  cdleme39a  39639  cdleme42b  39652  cdleme43dN  39666  cdlemeg47rv2  39684  cdlemeg46sfg  39694  cdlemeg46rjgN  39696  cdlemeg46rgv  39702  cdlemeg46req  39703  cdlemeg46gfv  39704  cdleme48d  39709  cdleme50ltrn  39731  cdlemf1  39735  cdlemf  39737  cdlemg2dN  39764  cdlemg2fvlem  39768  cdlemg2l  39777  cdlemg7fvbwN  39781  cdlemg7aN  39799  cdlemg10c  39813  cdlemg17a  39835  cdlemg17dALTN  39838  cdlemg18a  39852  cdlemg18b  39853  cdlemg31b0a  39869  cdlemg31a  39871  cdlemg31b  39872  ltrnco  39893  cdlemg48  39911  tgrpov  39922  tendoco2  39942  tendoplco2  39953  cdlemh1  39989  cdlemk1  40005  cdlemk26b-3  40079  cdlemk27-3  40081  cdlemk28-3  40082  cdlemk34  40084  cdlemkfid1N  40095  cdlemkid3N  40107  cdlemkid4  40108  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk51  40127  tendospcanN  40197  cdlemm10N  40292  dicvaddcl  40364  dicvscacl  40365  cdlemn6  40376  dihvalcq2  40421  dihord6b  40434  dihord5apre  40436  dihglbcpreN  40474  dihjatc1  40485  dihmeetlem20N  40500  dih1dimatlem0  40502  dihglblem6  40514  dochexmidlem4  40637  mapdpglem32  40879  mapdh8ad  40953  mapdh9aOLDN  40964  hdmap11lem2  41016  hdmap14lem6  41047  frlmfzowrdb  41384  mzpmfp  41787  mzpsubst  41788  pellex  41875  pellfundex  41926  pellfund14gap  41927  qirropth  41948  rmxypos  41988  congmul  42008  congsub  42011  mzpcong  42013  coprmdvdsb  42026  jm2.15nn0  42044  jm2.16nn0  42045  rpnnen3lem  42072  idomsubgmo  42242  relexp01min  42766  mullimc  44631  islptre  44634  mullimcf  44638  addlimc  44663  0ellimcdiv  44664  limsupre3lem  44747  limsupre3uzlem  44750  fourierdlem48  45169  fourierdlem80  45201  opnvonmbllem2  45648  ovolval5lem3  45669  ovnovollem3  45673  mapprop  47111  lincfsuppcl  47182  lindslinindimp2lem3  47229  itsclc0lem1  47530  itsclc0lem2  47531  itschlc0yqe  47534  itsclc0xyqsolr  47543