Theorem simp3r 1215

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  simp13r  1302  simp23r  1308  simp33r  1314  f1oiso2  7330  tfisi  7833  tfrlem5  8343  omeulem1  8544  omeulem2  8545  elfiun  9369  isfin2-2  10269  addlid  11359  mulcan  11817  mulcan2  11818  divass  11856  divdir  11863  div11OLD  11867  ltdiv1  12049  ltmuldiv  12058  lediv2  12075  xaddass2  13246  xlt2add  13256  expaddz  14112  expmulz  14114  resqrex  15267  resqrtcl  15270  o1add  15631  o1mul  15632  o1sub  15633  dvdsgcd  16568  rpexp12i  16749  pythagtriplem4  16845  pythagtriplem11  16851  pythagtriplem13  16853  pcpremul  16869  pceu  16872  pcqmul  16879  pcqdiv  16883  f1ocpbllem  17544  funcoppc  17898  funcres  17919  catcisolem  18133  1stfcl  18219  2ndfcl  18220  prfcl  18225  evlfcl  18244  curf1cl  18250  curfcl  18254  hofcl  18281  latjlej12  18477  latmlem12  18493  latj4  18511  latj4rot  18512  symgsssg  19497  symgfisg  19498  odcong  19579  cmn4  19831  ablsub4  19840  abladdsub4  19841  lsm4  19890  abvdom  20866  abvtrivd  20868  orngmul  20901  lspsolvlem  21199  lbsextlem2  21216  lidlsubcl  21281  frlmbas3  21815  matinvgcell  22482  matmulcell  22492  ma1repveval  22618  mdetunilem3  22661  mdetuni0  22668  mdetmul  22670  hausflimlem  24026  psmetlecl  24362  xmetlecl  24393  prdsxmetlem  24415  xblcntrps  24457  xblcntr  24458  bndth  25007  cph2ass  25262  iscau3  25327  dvres2  25961  coemullem  26297  vieta1  26363  aalioulem4  26386  cxpcn3lem  26799  angcan  26854  divsqrtsumlem  27031  dchrmusumlema  27544  dchrvmasumlema  27551  dchrisum0lema  27565  logdivsum  27584  padicabv  27681  cofcut1  28000  cofcut2  28002  divmulsw  28273  precsexlem8  28294  precsexlem9  28295  bdayfinbndlem1  28547  ax5seglem3  29088  ax5seglem6  29091  axpasch  29098  axeuclid  29120  axcontlem4  29124  axcontlem8  29128  trlsonistrl  29863  pthonispth  29902  spthonisspth  29906  wspthneq1eq2  30016  frgr2wwlkeqm  30489  adjlnop  32245  xreceu  33059  rhmdvd  33470  measvunilem  34469  measvuni  34471  bnj1128  35245  umgr2cycl  35451  satfv1fvfmla1  35733  cgrcomim  36299  cgrcoml  36306  cgrcomr  36307  cgrdegen  36314  segconeu  36321  btwnintr  36329  btwnexch3  36330  btwnouttr2  36332  btwnouttr  36334  btwnexch  36335  ifscgr  36354  lineext  36386  linecgr  36391  lineid  36393  idinside  36394  btwnconn1lem3  36399  btwnconn1lem4  36400  btwnconn1lem14  36410  btwnconn2  36412  btwnconn3  36413  midofsegid  36414  btwnoutside  36435  outsideoftr  36439  lineunray  36457  lineelsb2  36458  itg2addnclem  38130  cnres2  38222  heibor  38280  lsmcv2  39613  lcvat  39614  lcvexchlem4  39621  lcvexchlem5  39622  lfladd  39650  lflsub  39651  lflmul  39652  lshpkrlem4  39697  latm4  39817  omlmod1i2N  39844  cvlsupr7  39932  cvlsupr8  39933  hlatj4  39958  hlrelat3  39996  cvrval3  39997  atcvrj1  40015  atlelt  40022  2atlt  40023  2atjm  40029  3noncolr2  40033  athgt  40040  3dimlem2  40043  3dimlem4OLDN  40049  1cvratex  40057  ps-1  40061  ps-2  40062  hlatexch3N  40064  llnle  40102  atcvrlln2  40103  atcvrlln  40104  lplni2  40121  lplnle  40124  lplnnle2at  40125  lplnnlelln  40127  llncvrlpln2  40141  2llnmeqat  40155  lvolnle3at  40166  lvolnlelln  40168  4atlem0ae  40178  lneq2at  40362  lnjatN  40364  lncvrat  40366  2lnat  40368  elpaddri  40386  paddasslem2  40405  padd4N  40424  hlmod1i  40440  llnexchb2  40453  dalawlem2  40456  pclfinN  40484  pexmidlem4N  40557  pl42lem1N  40563  lhp2lt  40585  lhpexle1  40592  lhpexle2lem  40593  lhpj1  40606  lhpmcvr5N  40611  lhp2at0  40616  lhp2at0nle  40619  lhple  40626  lhpat  40627  lhpat4N  40628  4atexlemnslpq  40640  4atexlem7  40659  ltrn11  40710  ltrnle  40713  ltrnm  40715  ltrnj  40716  ltrncvr  40717  ltrnel  40723  ltrncnvel  40726  ltrncnv  40730  trlat  40753  trl0  40754  trlnidat  40757  trlnid  40763  ltrnatlw  40767  trlne  40769  trlval4  40772  cdlemc5  40779  cdlemd2  40783  cdlemd7  40788  cdlemd8  40789  cdlemd9  40790  cdleme0c  40797  cdleme0e  40801  cdleme0fN  40802  cdleme3g  40818  cdleme3h  40819  cdleme5  40824  cdleme11c  40845  cdleme11h  40850  cdleme11j  40851  cdleme11k  40852  cdleme0nex  40874  cdleme18a  40875  cdleme22gb  40878  cdleme20zN  40885  cdleme20c  40895  cdleme20k  40903  cdleme21a  40909  cdleme21b  40910  cdleme21c  40911  cdleme21ct  40913  cdleme21h  40918  cdleme22d  40927  cdleme22f  40930  cdleme26ee  40944  cdleme30a  40962  cdlemefs45eN  41015  cdleme36a  41044  cdleme36m  41045  cdleme39a  41049  cdleme42b  41062  cdleme43dN  41076  cdlemeg47rv2  41094  cdlemeg46sfg  41104  cdlemeg46rjgN  41106  cdlemeg46rgv  41112  cdlemeg46req  41113  cdlemeg46gfv  41114  cdleme48d  41119  cdleme50ltrn  41141  cdlemf1  41145  cdlemf  41147  cdlemg2dN  41174  cdlemg2fvlem  41178  cdlemg2l  41187  cdlemg7fvbwN  41191  cdlemg7aN  41209  cdlemg10c  41223  cdlemg17a  41245  cdlemg17dALTN  41248  cdlemg18a  41262  cdlemg18b  41263  cdlemg31b0a  41279  cdlemg31a  41281  cdlemg31b  41282  ltrnco  41303  cdlemg48  41321  tgrpov  41332  tendoco2  41352  tendoplco2  41363  cdlemh1  41399  cdlemk1  41415  cdlemk26b-3  41489  cdlemk27-3  41491  cdlemk28-3  41492  cdlemk34  41494  cdlemkfid1N  41505  cdlemkid3N  41517  cdlemkid4  41518  cdlemk35s-id  41522  cdlemk39s-id  41524  cdlemk51  41537  tendospcanN  41607  cdlemm10N  41702  dicvaddcl  41774  dicvscacl  41775  cdlemn6  41786  dihvalcq2  41831  dihord6b  41844  dihord5apre  41846  dihglbcpreN  41884  dihjatc1  41895  dihmeetlem20N  41910  dih1dimatlem0  41912  dihglblem6  41924  dochexmidlem4  42047  mapdpglem32  42289  mapdh8ad  42363  mapdh9aOLDN  42374  hdmap11lem2  42426  hdmap14lem6  42457  frlmfzowrdb  43086  mzpmfp  43288  mzpsubst  43289  pellex  43372  pellfundex  43423  pellfund14gap  43424  qirropth  43445  rmxypos  43484  congmul  43504  congsub  43507  mzpcong  43509  coprmdvdsb  43522  jm2.15nn0  43540  jm2.16nn0  43541  rpnnen3lem  43568  idomsubgmo  43730  relexp01min  44249  mullimc  46152  islptre  46155  mullimcf  46159  addlimc  46182  0ellimcdiv  46183  limsupre3lem  46266  limsupre3uzlem  46269  fourierdlem48  46688  fourierdlem80  46720  opnvonmbllem2  47167  ovolval5lem3  47188  ovnovollem3  47192  difltmodne  47902  isubgr3stgrlem1  48548  grlimedgclnbgr  48577  mapprop  48928  lincfsuppcl  48995  lindslinindimp2lem3  49042  itsclc0lem1  49338  itsclc0lem2  49339  itschlc0yqe  49342  itsclc0xyqsolr  49351  swapffunc  49863  fucofunc  49940  fucoppc  49991