Theorem simp3r 1201

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp13r  1288  simp23r  1294  simp33r  1300  f1oiso2  7372  tfisi  7880  tfrlem5  8419  omeulem1  8619  omeulem2  8620  elfiun  9468  isfin2-2  10357  addlid  11442  mulcan  11898  mulcan2  11899  divass  11938  divdir  11945  div11OLD  11949  ltdiv1  12130  ltmuldiv  12139  lediv2  12156  xaddass2  13289  xlt2add  13299  expaddz  14144  expmulz  14146  resqrex  15286  resqrtcl  15289  o1add  15647  o1mul  15648  o1sub  15649  dvdsgcd  16578  rpexp12i  16758  pythagtriplem4  16853  pythagtriplem11  16859  pythagtriplem13  16861  pcpremul  16877  pceu  16880  pcqmul  16887  pcqdiv  16891  f1ocpbllem  17571  funcoppc  17926  funcres  17947  catcisolem  18164  1stfcl  18253  2ndfcl  18254  prfcl  18259  evlfcl  18279  curf1cl  18285  curfcl  18289  hofcl  18316  latjlej12  18513  latmlem12  18529  latj4  18547  latj4rot  18548  symgsssg  19500  symgfisg  19501  odcong  19582  cmn4  19834  ablsub4  19843  abladdsub4  19844  lsm4  19893  abvdom  20848  abvtrivd  20850  lspsolvlem  21162  lbsextlem2  21179  lidlsubcl  21252  frlmbas3  21814  matinvgcell  22457  matmulcell  22467  ma1repveval  22593  mdetunilem3  22636  mdetuni0  22643  mdetmul  22645  hausflimlem  24003  psmetlecl  24341  xmetlecl  24372  prdsxmetlem  24394  xblcntrps  24436  xblcntr  24437  bndth  25004  cph2ass  25261  iscau3  25326  dvres2  25962  coemullem  26304  vieta1  26369  aalioulem4  26392  cxpcn3lem  26805  angcan  26860  divsqrtsumlem  27038  dchrmusumlema  27552  dchrvmasumlema  27559  dchrisum0lema  27573  logdivsum  27592  padicabv  27689  cofcut1  27969  cofcut2  27971  divsmulw  28233  precsexlem8  28253  precsexlem9  28254  ax5seglem3  28961  ax5seglem6  28964  axpasch  28971  axeuclid  28993  axcontlem4  28997  axcontlem8  29001  trlsonistrl  29742  pthonispth  29779  spthonisspth  29783  wspthneq1eq2  29890  frgr2wwlkeqm  30360  adjlnop  32115  xreceu  32889  orngmul  33313  rhmdvd  33328  measvunilem  34193  measvuni  34195  bnj1128  34983  umgr2cycl  35126  satfv1fvfmla1  35408  cgrcomim  35971  cgrcoml  35978  cgrcomr  35979  cgrdegen  35986  segconeu  35993  btwnintr  36001  btwnexch3  36002  btwnouttr2  36004  btwnouttr  36006  btwnexch  36007  ifscgr  36026  lineext  36058  linecgr  36063  lineid  36065  idinside  36066  btwnconn1lem3  36071  btwnconn1lem4  36072  btwnconn1lem14  36082  btwnconn2  36084  btwnconn3  36085  midofsegid  36086  btwnoutside  36107  outsideoftr  36111  lineunray  36129  lineelsb2  36130  itg2addnclem  37658  cnres2  37750  heibor  37808  lsmcv2  39011  lcvat  39012  lcvexchlem4  39019  lcvexchlem5  39020  lfladd  39048  lflsub  39049  lflmul  39050  lshpkrlem4  39095  latm4  39215  omlmod1i2N  39242  cvlsupr7  39330  cvlsupr8  39331  hlatj4  39356  hlrelat3  39395  cvrval3  39396  atcvrj1  39414  atlelt  39421  2atlt  39422  2atjm  39428  3noncolr2  39432  athgt  39439  3dimlem2  39442  3dimlem4OLDN  39448  1cvratex  39456  ps-1  39460  ps-2  39461  hlatexch3N  39463  llnle  39501  atcvrlln2  39502  atcvrlln  39503  lplni2  39520  lplnle  39523  lplnnle2at  39524  lplnnlelln  39526  llncvrlpln2  39540  2llnmeqat  39554  lvolnle3at  39565  lvolnlelln  39567  4atlem0ae  39577  lneq2at  39761  lnjatN  39763  lncvrat  39765  2lnat  39767  elpaddri  39785  paddasslem2  39804  padd4N  39823  hlmod1i  39839  llnexchb2  39852  dalawlem2  39855  pclfinN  39883  pexmidlem4N  39956  pl42lem1N  39962  lhp2lt  39984  lhpexle1  39991  lhpexle2lem  39992  lhpj1  40005  lhpmcvr5N  40010  lhp2at0  40015  lhp2at0nle  40018  lhple  40025  lhpat  40026  lhpat4N  40027  4atexlemnslpq  40039  4atexlem7  40058  ltrn11  40109  ltrnle  40112  ltrnm  40114  ltrnj  40115  ltrncvr  40116  ltrnel  40122  ltrncnvel  40125  ltrncnv  40129  trlat  40152  trl0  40153  trlnidat  40156  trlnid  40162  ltrnatlw  40166  trlne  40168  trlval4  40171  cdlemc5  40178  cdlemd2  40182  cdlemd7  40187  cdlemd8  40188  cdlemd9  40189  cdleme0c  40196  cdleme0e  40200  cdleme0fN  40201  cdleme3g  40217  cdleme3h  40218  cdleme5  40223  cdleme11c  40244  cdleme11h  40249  cdleme11j  40250  cdleme11k  40251  cdleme0nex  40273  cdleme18a  40274  cdleme22gb  40277  cdleme20zN  40284  cdleme20c  40294  cdleme20k  40302  cdleme21a  40308  cdleme21b  40309  cdleme21c  40310  cdleme21ct  40312  cdleme21h  40317  cdleme22d  40326  cdleme22f  40329  cdleme26ee  40343  cdleme30a  40361  cdlemefs45eN  40414  cdleme36a  40443  cdleme36m  40444  cdleme39a  40448  cdleme42b  40461  cdleme43dN  40475  cdlemeg47rv2  40493  cdlemeg46sfg  40503  cdlemeg46rjgN  40505  cdlemeg46rgv  40511  cdlemeg46req  40512  cdlemeg46gfv  40513  cdleme48d  40518  cdleme50ltrn  40540  cdlemf1  40544  cdlemf  40546  cdlemg2dN  40573  cdlemg2fvlem  40577  cdlemg2l  40586  cdlemg7fvbwN  40590  cdlemg7aN  40608  cdlemg10c  40622  cdlemg17a  40644  cdlemg17dALTN  40647  cdlemg18a  40661  cdlemg18b  40662  cdlemg31b0a  40678  cdlemg31a  40680  cdlemg31b  40681  ltrnco  40702  cdlemg48  40720  tgrpov  40731  tendoco2  40751  tendoplco2  40762  cdlemh1  40798  cdlemk1  40814  cdlemk26b-3  40888  cdlemk27-3  40890  cdlemk28-3  40891  cdlemk34  40893  cdlemkfid1N  40904  cdlemkid3N  40916  cdlemkid4  40917  cdlemk35s-id  40921  cdlemk39s-id  40923  cdlemk51  40936  tendospcanN  41006  cdlemm10N  41101  dicvaddcl  41173  dicvscacl  41174  cdlemn6  41185  dihvalcq2  41230  dihord6b  41243  dihord5apre  41245  dihglbcpreN  41283  dihjatc1  41294  dihmeetlem20N  41309  dih1dimatlem0  41311  dihglblem6  41323  dochexmidlem4  41446  mapdpglem32  41688  mapdh8ad  41762  mapdh9aOLDN  41773  hdmap11lem2  41825  hdmap14lem6  41856  frlmfzowrdb  42491  mzpmfp  42735  mzpsubst  42736  pellex  42823  pellfundex  42874  pellfund14gap  42875  qirropth  42896  rmxypos  42936  congmul  42956  congsub  42959  mzpcong  42961  coprmdvdsb  42974  jm2.15nn0  42992  jm2.16nn0  42993  rpnnen3lem  43020  idomsubgmo  43182  relexp01min  43703  mullimc  45572  islptre  45575  mullimcf  45579  addlimc  45604  0ellimcdiv  45605  limsupre3lem  45688  limsupre3uzlem  45691  fourierdlem48  46110  fourierdlem80  46142  opnvonmbllem2  46589  ovolval5lem3  46610  ovnovollem3  46614  difltmodne  47282  isubgr3stgrlem1  47869  mapprop  48191  lincfsuppcl  48259  lindslinindimp2lem3  48306  itsclc0lem1  48606  itsclc0lem2  48607  itschlc0yqe  48610  itsclc0xyqsolr  48619