MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3r Structured version   Visualization version   GIF version

Theorem simp3r 1089
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3r ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜃)

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 477 . 2 ((𝜒𝜃) → 𝜃)
213ad2ant3 1083 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
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 197  df-an 386  df-3an 1039
This theorem is referenced by:  simpl3r  1116  simpr3r  1122  simp13r  1176  simp23r  1182  simp33r  1188  f1oiso2  6599  tfisi  7055  tfrlem5  7473  omeulem1  7659  omeulem2  7660  elfiun  8333  isfin2-2  9138  addid2  10216  mulcan  10661  mulcan2  10662  divass  10700  divdir  10707  div11  10710  ltdiv1  10884  ltmuldiv  10893  lediv2  10910  xaddass2  12077  xlt2add  12087  expaddz  12899  expmulz  12901  resqrex  13985  resqrtcl  13988  o1add  14338  o1mul  14339  o1sub  14340  dvdsgcd  15255  rpexp12i  15428  pythagtriplem4  15518  pythagtriplem11  15524  pythagtriplem13  15526  pcpremul  15542  pceu  15545  pcqmul  15552  pcqdiv  15556  f1ocpbllem  16178  funcoppc  16529  funcres  16550  catcisolem  16750  1stfcl  16831  2ndfcl  16832  prfcl  16837  evlfcl  16856  curf1cl  16862  curfcl  16866  hofcl  16893  latjlej12  17061  latmlem12  17077  latj4  17095  latj4rot  17096  symgsssg  17881  symgfisg  17882  odcong  17962  cmn4  18206  ablsub4  18212  abladdsub4  18213  lsm4  18257  abvdom  18832  abvtrivd  18834  lspsolvlem  19136  lbsextlem2  19153  lidlsubcl  19210  frlmbas3  20109  matinvgcell  20235  matmulcell  20245  ma1repveval  20371  mdetunilem3  20414  mdetuni0  20421  mdetmul  20423  hausflimlem  21777  psmetlecl  22114  xmetlecl  22145  prdsxmetlem  22167  xblcntrps  22209  xblcntr  22210  bndth  22751  cph2ass  23007  iscau3  23070  dvres2  23670  coemullem  24000  vieta1  24061  aalioulem4  24084  cxpcn3lem  24482  angcan  24526  divsqrtsumlem  24700  dchrmusumlema  25176  dchrvmasumlema  25183  dchrisum0lema  25197  logdivsum  25216  padicabv  25313  ax5seglem3  25805  ax5seglem6  25808  axpasch  25815  axeuclid  25837  axcontlem4  25841  axcontlem8  25845  trlsonistrl  26599  pthonispth  26636  spthonisspth  26640  wspthneq1eq2  26739  frgr2wwlkeqm  27182  adjlnop  28929  xreceu  29615  orngmul  29788  rhmdvd  29806  measvunilem  30260  measvuni  30262  bnj1128  31043  cgrcomim  32080  cgrcoml  32087  cgrcomr  32088  cgrdegen  32095  segconeu  32102  btwnintr  32110  btwnexch3  32111  btwnouttr2  32113  btwnouttr  32115  btwnexch  32116  ifscgr  32135  lineext  32167  linecgr  32172  lineid  32174  idinside  32175  btwnconn1lem3  32180  btwnconn1lem4  32181  btwnconn1lem14  32191  btwnconn2  32193  btwnconn3  32194  midofsegid  32195  btwnoutside  32216  outsideoftr  32220  lineunray  32238  lineelsb2  32239  itg2addnclem  33441  cnres2  33542  heibor  33600  lsmcv2  34142  lcvat  34143  lcvexchlem4  34150  lcvexchlem5  34151  lfladd  34179  lflsub  34180  lflmul  34181  lshpkrlem4  34226  latm4  34346  omlmod1i2N  34373  cvlsupr7  34461  cvlsupr8  34462  hlatj4  34486  hlrelat3  34524  cvrval3  34525  atcvrj1  34543  atlelt  34550  2atlt  34551  2atjm  34557  3noncolr2  34561  athgt  34568  3dimlem2  34571  3dimlem4OLDN  34577  1cvratex  34585  ps-1  34589  ps-2  34590  hlatexch3N  34592  llnle  34630  atcvrlln2  34631  atcvrlln  34632  lplni2  34649  lplnle  34652  lplnnle2at  34653  lplnnlelln  34655  llncvrlpln2  34669  2llnmeqat  34683  lvolnle3at  34694  lvolnlelln  34696  4atlem0ae  34706  lneq2at  34890  lnjatN  34892  lncvrat  34894  2lnat  34896  elpaddri  34914  paddasslem2  34933  padd4N  34952  hlmod1i  34968  llnexchb2  34981  dalawlem2  34984  pclfinN  35012  pexmidlem4N  35085  pl42lem1N  35091  lhp2lt  35113  lhpexle1  35120  lhpexle2lem  35121  lhpj1  35134  lhpmcvr5N  35139  lhp2at0  35144  lhp2at0nle  35147  lhple  35154  lhpat  35155  lhpat4N  35156  4atexlemnslpq  35168  4atexlem7  35187  ltrn11  35238  ltrnle  35241  ltrnm  35243  ltrnj  35244  ltrncvr  35245  ltrnel  35251  ltrncnvel  35254  ltrncnv  35258  ltrnmwOLD  35264  trlat  35282  trl0  35283  trlnidat  35286  trlnid  35292  ltrnatlw  35296  trlne  35298  trlval4  35301  cdlemc5  35308  cdlemd2  35312  cdlemd7  35317  cdlemd8  35318  cdlemd9  35319  cdleme0c  35326  cdleme0e  35330  cdleme0fN  35331  cdleme3g  35347  cdleme3h  35348  cdleme5  35353  cdleme11c  35374  cdleme11h  35379  cdleme11j  35380  cdleme11k  35381  cdleme0nex  35403  cdleme18a  35404  cdleme22gb  35407  cdleme20zN  35414  cdleme20yOLD  35416  cdleme20c  35425  cdleme20k  35433  cdleme21a  35439  cdleme21b  35440  cdleme21c  35441  cdleme21ct  35443  cdleme21h  35448  cdleme22d  35457  cdleme22f  35460  cdleme26ee  35474  cdleme30a  35492  cdlemefs45eN  35545  cdleme36a  35574  cdleme36m  35575  cdleme39a  35579  cdleme42b  35592  cdleme43dN  35606  cdlemeg47rv2  35624  cdlemeg46sfg  35634  cdlemeg46rjgN  35636  cdlemeg46rgv  35642  cdlemeg46req  35643  cdlemeg46gfv  35644  cdleme48d  35649  cdleme50ltrn  35671  cdlemf1  35675  cdlemf  35677  cdlemg2dN  35704  cdlemg2fvlem  35708  cdlemg2l  35717  cdlemg7fvbwN  35721  cdlemg7aN  35739  cdlemg10c  35753  cdlemg17a  35775  cdlemg17dALTN  35778  cdlemg18a  35792  cdlemg18b  35793  cdlemg31b0a  35809  cdlemg31a  35811  cdlemg31b  35812  ltrnco  35833  cdlemg48  35851  tgrpov  35862  tendoco2  35882  tendoplco2  35893  cdlemh1  35929  cdlemk1  35945  cdlemk26b-3  36019  cdlemk27-3  36021  cdlemk28-3  36022  cdlemk34  36024  cdlemkfid1N  36035  cdlemkid3N  36047  cdlemkid4  36048  cdlemk35s-id  36052  cdlemk39s-id  36054  cdlemk51  36067  tendospcanN  36138  cdlemm10N  36233  dicvaddcl  36305  dicvscacl  36306  cdlemn6  36317  dihvalcq2  36362  dihord6b  36375  dihord5apre  36377  dihglbcpreN  36415  dihjatc1  36426  dihmeetlem20N  36441  dih1dimatlem0  36443  dihglblem6  36455  dochexmidlem4  36578  mapdpglem32  36820  mapdh8ad  36894  mapdh9aOLDN  36906  hdmap11lem2  36960  hdmap14lem6  36991  mzpmfp  37136  mzpsubst  37137  pellex  37225  pellfundex  37276  pellfund14gap  37277  qirropth  37299  rmxypos  37340  congmul  37360  congsub  37363  mzpcong  37365  coprmdvdsb  37378  jm2.15nn0  37396  jm2.16nn0  37397  rpnnen3lem  37424  idomsubgmo  37602  relexp01min  37831  mullimc  39654  islptre  39657  mullimcf  39661  addlimc  39686  0ellimcdiv  39687  limsupre3lem  39770  limsupre3uzlem  39773  fourierdlem48  40140  fourierdlem80  40172  opnvonmbllem2  40616  ovolval5lem3  40637  ovnovollem3  40641  lincfsuppcl  41973  lindslinindimp2lem3  42020
  Copyright terms: Public domain W3C validator