Theorem simp3r 1204

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 1137	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

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

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

This theorem is referenced by:  simp13r  1291  simp23r  1297  simp33r  1303  f1oiso2  7161  tfisi  7637  tfrlem5  8116  omeulem1  8310  omeulem2  8311  elfiun  9046  isfin2-2  9933  addid2  11015  mulcan  11469  mulcan2  11470  divass  11508  divdir  11515  div11  11518  ltdiv1  11696  ltmuldiv  11705  lediv2  11722  xaddass2  12840  xlt2add  12850  expaddz  13679  expmulz  13681  resqrex  14814  resqrtcl  14817  o1add  15175  o1mul  15176  o1sub  15177  dvdsgcd  16104  rpexp12i  16281  pythagtriplem4  16372  pythagtriplem11  16378  pythagtriplem13  16380  pcpremul  16396  pceu  16399  pcqmul  16406  pcqdiv  16410  f1ocpbllem  17029  funcoppc  17381  funcres  17402  catcisolem  17616  1stfcl  17704  2ndfcl  17705  prfcl  17710  evlfcl  17730  curf1cl  17736  curfcl  17740  hofcl  17767  latjlej12  17961  latmlem12  17977  latj4  17995  latj4rot  17996  symgsssg  18859  symgfisg  18860  odcong  18941  cmn4  19190  ablsub4  19198  abladdsub4  19199  lsm4  19245  abvdom  19874  abvtrivd  19876  lspsolvlem  20179  lbsextlem2  20196  lidlsubcl  20254  frlmbas3  20738  matinvgcell  21332  matmulcell  21342  ma1repveval  21468  mdetunilem3  21511  mdetuni0  21518  mdetmul  21520  hausflimlem  22876  psmetlecl  23213  xmetlecl  23244  prdsxmetlem  23266  xblcntrps  23308  xblcntr  23309  bndth  23855  cph2ass  24110  iscau3  24175  dvres2  24809  coemullem  25144  vieta1  25205  aalioulem4  25228  cxpcn3lem  25633  angcan  25685  divsqrtsumlem  25862  dchrmusumlema  26374  dchrvmasumlema  26381  dchrisum0lema  26395  logdivsum  26414  padicabv  26511  ax5seglem3  27022  ax5seglem6  27025  axpasch  27032  axeuclid  27054  axcontlem4  27058  axcontlem8  27062  trlsonistrl  27796  pthonispth  27833  spthonisspth  27837  wspthneq1eq2  27944  frgr2wwlkeqm  28414  adjlnop  30167  xreceu  30916  orngmul  31221  rhmdvd  31239  measvunilem  31892  measvuni  31894  bnj1128  32683  umgr2cycl  32816  satfv1fvfmla1  33098  cofcut1  33827  cofcut2  33828  cgrcomim  34028  cgrcoml  34035  cgrcomr  34036  cgrdegen  34043  segconeu  34050  btwnintr  34058  btwnexch3  34059  btwnouttr2  34061  btwnouttr  34063  btwnexch  34064  ifscgr  34083  lineext  34115  linecgr  34120  lineid  34122  idinside  34123  btwnconn1lem3  34128  btwnconn1lem4  34129  btwnconn1lem14  34139  btwnconn2  34141  btwnconn3  34142  midofsegid  34143  btwnoutside  34164  outsideoftr  34168  lineunray  34186  lineelsb2  34187  itg2addnclem  35565  cnres2  35658  heibor  35716  lsmcv2  36780  lcvat  36781  lcvexchlem4  36788  lcvexchlem5  36789  lfladd  36817  lflsub  36818  lflmul  36819  lshpkrlem4  36864  latm4  36984  omlmod1i2N  37011  cvlsupr7  37099  cvlsupr8  37100  hlatj4  37125  hlrelat3  37163  cvrval3  37164  atcvrj1  37182  atlelt  37189  2atlt  37190  2atjm  37196  3noncolr2  37200  athgt  37207  3dimlem2  37210  3dimlem4OLDN  37216  1cvratex  37224  ps-1  37228  ps-2  37229  hlatexch3N  37231  llnle  37269  atcvrlln2  37270  atcvrlln  37271  lplni2  37288  lplnle  37291  lplnnle2at  37292  lplnnlelln  37294  llncvrlpln2  37308  2llnmeqat  37322  lvolnle3at  37333  lvolnlelln  37335  4atlem0ae  37345  lneq2at  37529  lnjatN  37531  lncvrat  37533  2lnat  37535  elpaddri  37553  paddasslem2  37572  padd4N  37591  hlmod1i  37607  llnexchb2  37620  dalawlem2  37623  pclfinN  37651  pexmidlem4N  37724  pl42lem1N  37730  lhp2lt  37752  lhpexle1  37759  lhpexle2lem  37760  lhpj1  37773  lhpmcvr5N  37778  lhp2at0  37783  lhp2at0nle  37786  lhple  37793  lhpat  37794  lhpat4N  37795  4atexlemnslpq  37807  4atexlem7  37826  ltrn11  37877  ltrnle  37880  ltrnm  37882  ltrnj  37883  ltrncvr  37884  ltrnel  37890  ltrncnvel  37893  ltrncnv  37897  trlat  37920  trl0  37921  trlnidat  37924  trlnid  37930  ltrnatlw  37934  trlne  37936  trlval4  37939  cdlemc5  37946  cdlemd2  37950  cdlemd7  37955  cdlemd8  37956  cdlemd9  37957  cdleme0c  37964  cdleme0e  37968  cdleme0fN  37969  cdleme3g  37985  cdleme3h  37986  cdleme5  37991  cdleme11c  38012  cdleme11h  38017  cdleme11j  38018  cdleme11k  38019  cdleme0nex  38041  cdleme18a  38042  cdleme22gb  38045  cdleme20zN  38052  cdleme20c  38062  cdleme20k  38070  cdleme21a  38076  cdleme21b  38077  cdleme21c  38078  cdleme21ct  38080  cdleme21h  38085  cdleme22d  38094  cdleme22f  38097  cdleme26ee  38111  cdleme30a  38129  cdlemefs45eN  38182  cdleme36a  38211  cdleme36m  38212  cdleme39a  38216  cdleme42b  38229  cdleme43dN  38243  cdlemeg47rv2  38261  cdlemeg46sfg  38271  cdlemeg46rjgN  38273  cdlemeg46rgv  38279  cdlemeg46req  38280  cdlemeg46gfv  38281  cdleme48d  38286  cdleme50ltrn  38308  cdlemf1  38312  cdlemf  38314  cdlemg2dN  38341  cdlemg2fvlem  38345  cdlemg2l  38354  cdlemg7fvbwN  38358  cdlemg7aN  38376  cdlemg10c  38390  cdlemg17a  38412  cdlemg17dALTN  38415  cdlemg18a  38429  cdlemg18b  38430  cdlemg31b0a  38446  cdlemg31a  38448  cdlemg31b  38449  ltrnco  38470  cdlemg48  38488  tgrpov  38499  tendoco2  38519  tendoplco2  38530  cdlemh1  38566  cdlemk1  38582  cdlemk26b-3  38656  cdlemk27-3  38658  cdlemk28-3  38659  cdlemk34  38661  cdlemkfid1N  38672  cdlemkid3N  38684  cdlemkid4  38685  cdlemk35s-id  38689  cdlemk39s-id  38691  cdlemk51  38704  tendospcanN  38774  cdlemm10N  38869  dicvaddcl  38941  dicvscacl  38942  cdlemn6  38953  dihvalcq2  38998  dihord6b  39011  dihord5apre  39013  dihglbcpreN  39051  dihjatc1  39062  dihmeetlem20N  39077  dih1dimatlem0  39079  dihglblem6  39091  dochexmidlem4  39214  mapdpglem32  39456  mapdh8ad  39530  mapdh9aOLDN  39541  hdmap11lem2  39593  hdmap14lem6  39624  frlmfzowrdb  39948  mzpmfp  40272  mzpsubst  40273  pellex  40360  pellfundex  40411  pellfund14gap  40412  qirropth  40433  rmxypos  40472  congmul  40492  congsub  40495  mzpcong  40497  coprmdvdsb  40510  jm2.15nn0  40528  jm2.16nn0  40529  rpnnen3lem  40556  idomsubgmo  40726  relexp01min  40998  mullimc  42832  islptre  42835  mullimcf  42839  addlimc  42864  0ellimcdiv  42865  limsupre3lem  42948  limsupre3uzlem  42951  fourierdlem48  43370  fourierdlem80  43402  opnvonmbllem2  43846  ovolval5lem3  43867  ovnovollem3  43871  mapprop  45355  lincfsuppcl  45427  lindslinindimp2lem3  45474  itsclc0lem1  45775  itsclc0lem2  45776  itschlc0yqe  45779  itsclc0xyqsolr  45788