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

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

This theorem is referenced by:  simp13r  1291  simp23r  1297  simp33r  1303  f1oiso2  7308  tfisi  7811  tfrlem5  8321  omeulem1  8519  omeulem2  8520  elfiun  9345  isfin2-2  10241  addlid  11328  mulcan  11786  mulcan2  11787  divass  11826  divdir  11833  div11OLD  11837  ltdiv1  12018  ltmuldiv  12027  lediv2  12044  xaddass2  13177  xlt2add  13187  expaddz  14041  expmulz  14043  resqrex  15185  resqrtcl  15188  o1add  15549  o1mul  15550  o1sub  15551  dvdsgcd  16483  rpexp12i  16663  pythagtriplem4  16759  pythagtriplem11  16765  pythagtriplem13  16767  pcpremul  16783  pceu  16786  pcqmul  16793  pcqdiv  16797  f1ocpbllem  17457  funcoppc  17811  funcres  17832  catcisolem  18046  1stfcl  18132  2ndfcl  18133  prfcl  18138  evlfcl  18157  curf1cl  18163  curfcl  18167  hofcl  18194  latjlej12  18390  latmlem12  18406  latj4  18424  latj4rot  18425  symgsssg  19408  symgfisg  19409  odcong  19490  cmn4  19742  ablsub4  19751  abladdsub4  19752  lsm4  19801  abvdom  20775  abvtrivd  20777  orngmul  20810  lspsolvlem  21109  lbsextlem2  21126  lidlsubcl  21191  frlmbas3  21743  matinvgcell  22391  matmulcell  22401  ma1repveval  22527  mdetunilem3  22570  mdetuni0  22577  mdetmul  22579  hausflimlem  23935  psmetlecl  24271  xmetlecl  24302  prdsxmetlem  24324  xblcntrps  24366  xblcntr  24367  bndth  24925  cph2ass  25181  iscau3  25246  dvres2  25881  coemullem  26223  vieta1  26288  aalioulem4  26311  cxpcn3lem  26725  angcan  26780  divsqrtsumlem  26958  dchrmusumlema  27472  dchrvmasumlema  27479  dchrisum0lema  27493  logdivsum  27512  padicabv  27609  cofcut1  27928  cofcut2  27930  divmulsw  28201  precsexlem8  28222  precsexlem9  28223  bdayfinbndlem1  28475  ax5seglem3  29016  ax5seglem6  29019  axpasch  29026  axeuclid  29048  axcontlem4  29052  axcontlem8  29056  trlsonistrl  29792  pthonispth  29831  spthonisspth  29835  wspthneq1eq2  29945  frgr2wwlkeqm  30418  adjlnop  32173  xreceu  33013  rhmdvd  33416  measvunilem  34389  measvuni  34391  bnj1128  35165  umgr2cycl  35354  satfv1fvfmla1  35636  cgrcomim  36202  cgrcoml  36209  cgrcomr  36210  cgrdegen  36217  segconeu  36224  btwnintr  36232  btwnexch3  36233  btwnouttr2  36235  btwnouttr  36237  btwnexch  36238  ifscgr  36257  lineext  36289  linecgr  36294  lineid  36296  idinside  36297  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem14  36313  btwnconn2  36315  btwnconn3  36316  midofsegid  36317  btwnoutside  36338  outsideoftr  36342  lineunray  36360  lineelsb2  36361  itg2addnclem  37919  cnres2  38011  heibor  38069  lsmcv2  39402  lcvat  39403  lcvexchlem4  39410  lcvexchlem5  39411  lfladd  39439  lflsub  39440  lflmul  39441  lshpkrlem4  39486  latm4  39606  omlmod1i2N  39633  cvlsupr7  39721  cvlsupr8  39722  hlatj4  39747  hlrelat3  39785  cvrval3  39786  atcvrj1  39804  atlelt  39811  2atlt  39812  2atjm  39818  3noncolr2  39822  athgt  39829  3dimlem2  39832  3dimlem4OLDN  39838  1cvratex  39846  ps-1  39850  ps-2  39851  hlatexch3N  39853  llnle  39891  atcvrlln2  39892  atcvrlln  39893  lplni2  39910  lplnle  39913  lplnnle2at  39914  lplnnlelln  39916  llncvrlpln2  39930  2llnmeqat  39944  lvolnle3at  39955  lvolnlelln  39957  4atlem0ae  39967  lneq2at  40151  lnjatN  40153  lncvrat  40155  2lnat  40157  elpaddri  40175  paddasslem2  40194  padd4N  40213  hlmod1i  40229  llnexchb2  40242  dalawlem2  40245  pclfinN  40273  pexmidlem4N  40346  pl42lem1N  40352  lhp2lt  40374  lhpexle1  40381  lhpexle2lem  40382  lhpj1  40395  lhpmcvr5N  40400  lhp2at0  40405  lhp2at0nle  40408  lhple  40415  lhpat  40416  lhpat4N  40417  4atexlemnslpq  40429  4atexlem7  40448  ltrn11  40499  ltrnle  40502  ltrnm  40504  ltrnj  40505  ltrncvr  40506  ltrnel  40512  ltrncnvel  40515  ltrncnv  40519  trlat  40542  trl0  40543  trlnidat  40546  trlnid  40552  ltrnatlw  40556  trlne  40558  trlval4  40561  cdlemc5  40568  cdlemd2  40572  cdlemd7  40577  cdlemd8  40578  cdlemd9  40579  cdleme0c  40586  cdleme0e  40590  cdleme0fN  40591  cdleme3g  40607  cdleme3h  40608  cdleme5  40613  cdleme11c  40634  cdleme11h  40639  cdleme11j  40640  cdleme11k  40641  cdleme0nex  40663  cdleme18a  40664  cdleme22gb  40667  cdleme20zN  40674  cdleme20c  40684  cdleme20k  40692  cdleme21a  40698  cdleme21b  40699  cdleme21c  40700  cdleme21ct  40702  cdleme21h  40707  cdleme22d  40716  cdleme22f  40719  cdleme26ee  40733  cdleme30a  40751  cdlemefs45eN  40804  cdleme36a  40833  cdleme36m  40834  cdleme39a  40838  cdleme42b  40851  cdleme43dN  40865  cdlemeg47rv2  40883  cdlemeg46sfg  40893  cdlemeg46rjgN  40895  cdlemeg46rgv  40901  cdlemeg46req  40902  cdlemeg46gfv  40903  cdleme48d  40908  cdleme50ltrn  40930  cdlemf1  40934  cdlemf  40936  cdlemg2dN  40963  cdlemg2fvlem  40967  cdlemg2l  40976  cdlemg7fvbwN  40980  cdlemg7aN  40998  cdlemg10c  41012  cdlemg17a  41034  cdlemg17dALTN  41037  cdlemg18a  41051  cdlemg18b  41052  cdlemg31b0a  41068  cdlemg31a  41070  cdlemg31b  41071  ltrnco  41092  cdlemg48  41110  tgrpov  41121  tendoco2  41141  tendoplco2  41152  cdlemh1  41188  cdlemk1  41204  cdlemk26b-3  41278  cdlemk27-3  41280  cdlemk28-3  41281  cdlemk34  41283  cdlemkfid1N  41294  cdlemkid3N  41306  cdlemkid4  41307  cdlemk35s-id  41311  cdlemk39s-id  41313  cdlemk51  41326  tendospcanN  41396  cdlemm10N  41491  dicvaddcl  41563  dicvscacl  41564  cdlemn6  41575  dihvalcq2  41620  dihord6b  41633  dihord5apre  41635  dihglbcpreN  41673  dihjatc1  41684  dihmeetlem20N  41699  dih1dimatlem0  41701  dihglblem6  41713  dochexmidlem4  41836  mapdpglem32  42078  mapdh8ad  42152  mapdh9aOLDN  42163  hdmap11lem2  42215  hdmap14lem6  42246  frlmfzowrdb  42871  mzpmfp  43101  mzpsubst  43102  pellex  43189  pellfundex  43240  pellfund14gap  43241  qirropth  43262  rmxypos  43301  congmul  43321  congsub  43324  mzpcong  43326  coprmdvdsb  43339  jm2.15nn0  43357  jm2.16nn0  43358  rpnnen3lem  43385  idomsubgmo  43547  relexp01min  44066  mullimc  45973  islptre  45976  mullimcf  45980  addlimc  46003  0ellimcdiv  46004  limsupre3lem  46087  limsupre3uzlem  46090  fourierdlem48  46509  fourierdlem80  46541  opnvonmbllem2  46988  ovolval5lem3  47009  ovnovollem3  47013  difltmodne  47699  isubgr3stgrlem1  48323  grlimedgclnbgr  48352  mapprop  48703  lincfsuppcl  48770  lindslinindimp2lem3  48817  itsclc0lem1  49113  itsclc0lem2  49114  itschlc0yqe  49117  itsclc0xyqsolr  49126  swapffunc  49638  fucofunc  49715  fucoppc  49766