Theorem simp3r 1210

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  simp13r  1297  simp23r  1303  simp33r  1309  f1oiso2  7300  tfisi  7803  tfrlem5  8313  omeulem1  8511  omeulem2  8512  elfiun  9337  isfin2-2  10236  addlid  11324  mulcan  11782  mulcan2  11783  divass  11822  divdir  11829  div11OLD  11833  ltdiv1  12015  ltmuldiv  12024  lediv2  12041  xaddass2  13197  xlt2add  13207  expaddz  14063  expmulz  14065  resqrex  15207  resqrtcl  15210  o1add  15571  o1mul  15572  o1sub  15573  dvdsgcd  16508  rpexp12i  16689  pythagtriplem4  16785  pythagtriplem11  16791  pythagtriplem13  16793  pcpremul  16809  pceu  16812  pcqmul  16819  pcqdiv  16823  f1ocpbllem  17483  funcoppc  17837  funcres  17858  catcisolem  18072  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  latjlej12  18416  latmlem12  18432  latj4  18450  latj4rot  18451  symgsssg  19437  symgfisg  19438  odcong  19519  cmn4  19771  ablsub4  19780  abladdsub4  19781  lsm4  19830  abvdom  20806  abvtrivd  20808  orngmul  20841  lspsolvlem  21139  lbsextlem2  21156  lidlsubcl  21221  frlmbas3  21755  matinvgcell  22422  matmulcell  22432  ma1repveval  22558  mdetunilem3  22601  mdetuni0  22608  mdetmul  22610  hausflimlem  23966  psmetlecl  24302  xmetlecl  24333  prdsxmetlem  24355  xblcntrps  24397  xblcntr  24398  bndth  24947  cph2ass  25202  iscau3  25267  dvres2  25901  coemullem  26237  vieta1  26300  aalioulem4  26323  cxpcn3lem  26733  angcan  26788  divsqrtsumlem  26965  dchrmusumlema  27478  dchrvmasumlema  27485  dchrisum0lema  27499  logdivsum  27518  padicabv  27615  cofcut1  27934  cofcut2  27936  divmulsw  28207  precsexlem8  28228  precsexlem9  28229  bdayfinbndlem1  28481  ax5seglem3  29022  ax5seglem6  29025  axpasch  29032  axeuclid  29054  axcontlem4  29058  axcontlem8  29062  trlsonistrl  29797  pthonispth  29836  spthonisspth  29840  wspthneq1eq2  29950  frgr2wwlkeqm  30423  adjlnop  32179  xreceu  33004  rhmdvd  33411  measvunilem  34408  measvuni  34410  bnj1128  35187  umgr2cycl  35384  satfv1fvfmla1  35666  cgrcomim  36232  cgrcoml  36239  cgrcomr  36240  cgrdegen  36247  segconeu  36254  btwnintr  36262  btwnexch3  36263  btwnouttr2  36265  btwnouttr  36267  btwnexch  36268  ifscgr  36287  lineext  36319  linecgr  36324  lineid  36326  idinside  36327  btwnconn1lem3  36332  btwnconn1lem4  36333  btwnconn1lem14  36343  btwnconn2  36345  btwnconn3  36346  midofsegid  36347  btwnoutside  36368  outsideoftr  36372  lineunray  36390  lineelsb2  36391  itg2addnclem  38053  cnres2  38145  heibor  38203  lsmcv2  39536  lcvat  39537  lcvexchlem4  39544  lcvexchlem5  39545  lfladd  39573  lflsub  39574  lflmul  39575  lshpkrlem4  39620  latm4  39740  omlmod1i2N  39767  cvlsupr7  39855  cvlsupr8  39856  hlatj4  39881  hlrelat3  39919  cvrval3  39920  atcvrj1  39938  atlelt  39945  2atlt  39946  2atjm  39952  3noncolr2  39956  athgt  39963  3dimlem2  39966  3dimlem4OLDN  39972  1cvratex  39980  ps-1  39984  ps-2  39985  hlatexch3N  39987  llnle  40025  atcvrlln2  40026  atcvrlln  40027  lplni2  40044  lplnle  40047  lplnnle2at  40048  lplnnlelln  40050  llncvrlpln2  40064  2llnmeqat  40078  lvolnle3at  40089  lvolnlelln  40091  4atlem0ae  40101  lneq2at  40285  lnjatN  40287  lncvrat  40289  2lnat  40291  elpaddri  40309  paddasslem2  40328  padd4N  40347  hlmod1i  40363  llnexchb2  40376  dalawlem2  40379  pclfinN  40407  pexmidlem4N  40480  pl42lem1N  40486  lhp2lt  40508  lhpexle1  40515  lhpexle2lem  40516  lhpj1  40529  lhpmcvr5N  40534  lhp2at0  40539  lhp2at0nle  40542  lhple  40549  lhpat  40550  lhpat4N  40551  4atexlemnslpq  40563  4atexlem7  40582  ltrn11  40633  ltrnle  40636  ltrnm  40638  ltrnj  40639  ltrncvr  40640  ltrnel  40646  ltrncnvel  40649  ltrncnv  40653  trlat  40676  trl0  40677  trlnidat  40680  trlnid  40686  ltrnatlw  40690  trlne  40692  trlval4  40695  cdlemc5  40702  cdlemd2  40706  cdlemd7  40711  cdlemd8  40712  cdlemd9  40713  cdleme0c  40720  cdleme0e  40724  cdleme0fN  40725  cdleme3g  40741  cdleme3h  40742  cdleme5  40747  cdleme11c  40768  cdleme11h  40773  cdleme11j  40774  cdleme11k  40775  cdleme0nex  40797  cdleme18a  40798  cdleme22gb  40801  cdleme20zN  40808  cdleme20c  40818  cdleme20k  40826  cdleme21a  40832  cdleme21b  40833  cdleme21c  40834  cdleme21ct  40836  cdleme21h  40841  cdleme22d  40850  cdleme22f  40853  cdleme26ee  40867  cdleme30a  40885  cdlemefs45eN  40938  cdleme36a  40967  cdleme36m  40968  cdleme39a  40972  cdleme42b  40985  cdleme43dN  40999  cdlemeg47rv2  41017  cdlemeg46sfg  41027  cdlemeg46rjgN  41029  cdlemeg46rgv  41035  cdlemeg46req  41036  cdlemeg46gfv  41037  cdleme48d  41042  cdleme50ltrn  41064  cdlemf1  41068  cdlemf  41070  cdlemg2dN  41097  cdlemg2fvlem  41101  cdlemg2l  41110  cdlemg7fvbwN  41114  cdlemg7aN  41132  cdlemg10c  41146  cdlemg17a  41168  cdlemg17dALTN  41171  cdlemg18a  41185  cdlemg18b  41186  cdlemg31b0a  41202  cdlemg31a  41204  cdlemg31b  41205  ltrnco  41226  cdlemg48  41244  tgrpov  41255  tendoco2  41275  tendoplco2  41286  cdlemh1  41322  cdlemk1  41338  cdlemk26b-3  41412  cdlemk27-3  41414  cdlemk28-3  41415  cdlemk34  41417  cdlemkfid1N  41428  cdlemkid3N  41440  cdlemkid4  41441  cdlemk35s-id  41445  cdlemk39s-id  41447  cdlemk51  41460  tendospcanN  41530  cdlemm10N  41625  dicvaddcl  41697  dicvscacl  41698  cdlemn6  41709  dihvalcq2  41754  dihord6b  41767  dihord5apre  41769  dihglbcpreN  41807  dihjatc1  41818  dihmeetlem20N  41833  dih1dimatlem0  41835  dihglblem6  41847  dochexmidlem4  41970  mapdpglem32  42212  mapdh8ad  42286  mapdh9aOLDN  42297  hdmap11lem2  42349  hdmap14lem6  42380  frlmfzowrdb  43009  mzpmfp  43211  mzpsubst  43212  pellex  43295  pellfundex  43346  pellfund14gap  43347  qirropth  43368  rmxypos  43407  congmul  43427  congsub  43430  mzpcong  43432  coprmdvdsb  43445  jm2.15nn0  43463  jm2.16nn0  43464  rpnnen3lem  43491  idomsubgmo  43653  relexp01min  44172  mullimc  46075  islptre  46078  mullimcf  46082  addlimc  46105  0ellimcdiv  46106  limsupre3lem  46189  limsupre3uzlem  46192  fourierdlem48  46611  fourierdlem80  46643  opnvonmbllem2  47090  ovolval5lem3  47111  ovnovollem3  47115  difltmodne  47825  isubgr3stgrlem1  48471  grlimedgclnbgr  48500  mapprop  48851  lincfsuppcl  48918  lindslinindimp2lem3  48965  itsclc0lem1  49261  itsclc0lem2  49262  itschlc0yqe  49265  itsclc0xyqsolr  49274  swapffunc  49786  fucofunc  49863  fucoppc  49914