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

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

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 476 . 2 ((𝜒𝜃) → 𝜃)
213ad2ant3 1104 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  simpl3r  1137  simpr3r  1143  simp13r  1197  simp23r  1203  simp33r  1209  f1oiso2  6642  tfisi  7100  tfrlem5  7521  omeulem1  7707  omeulem2  7708  elfiun  8377  isfin2-2  9179  addid2  10257  mulcan  10702  mulcan2  10703  divass  10741  divdir  10748  div11  10751  ltdiv1  10925  ltmuldiv  10934  lediv2  10951  xaddass2  12118  xlt2add  12128  expaddz  12944  expmulz  12946  resqrex  14035  resqrtcl  14038  o1add  14388  o1mul  14389  o1sub  14390  dvdsgcd  15308  rpexp12i  15481  pythagtriplem4  15571  pythagtriplem11  15577  pythagtriplem13  15579  pcpremul  15595  pceu  15598  pcqmul  15605  pcqdiv  15609  f1ocpbllem  16231  funcoppc  16582  funcres  16603  catcisolem  16803  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  curfcl  16919  hofcl  16946  latjlej12  17114  latmlem12  17130  latj4  17148  latj4rot  17149  symgsssg  17933  symgfisg  17934  odcong  18014  cmn4  18258  ablsub4  18264  abladdsub4  18265  lsm4  18309  abvdom  18886  abvtrivd  18888  lspsolvlem  19190  lbsextlem2  19207  lidlsubcl  19264  frlmbas3  20163  matinvgcell  20289  matmulcell  20299  ma1repveval  20425  mdetunilem3  20468  mdetuni0  20475  mdetmul  20477  hausflimlem  21830  psmetlecl  22167  xmetlecl  22198  prdsxmetlem  22220  xblcntrps  22262  xblcntr  22263  bndth  22804  cph2ass  23059  iscau3  23122  dvres2  23721  coemullem  24051  vieta1  24112  aalioulem4  24135  cxpcn3lem  24533  angcan  24577  divsqrtsumlem  24751  dchrmusumlema  25227  dchrvmasumlema  25234  dchrisum0lema  25248  logdivsum  25267  padicabv  25364  ax5seglem3  25856  ax5seglem6  25859  axpasch  25866  axeuclid  25888  axcontlem4  25892  axcontlem8  25896  trlsonistrl  26661  pthonispth  26698  spthonisspth  26702  wspthneq1eq2  26814  frgr2wwlkeqm  27311  adjlnop  29073  xreceu  29758  orngmul  29931  rhmdvd  29949  measvunilem  30403  measvuni  30405  bnj1128  31184  cgrcomim  32221  cgrcoml  32228  cgrcomr  32229  cgrdegen  32236  segconeu  32243  btwnintr  32251  btwnexch3  32252  btwnouttr2  32254  btwnouttr  32256  btwnexch  32257  ifscgr  32276  lineext  32308  linecgr  32313  lineid  32315  idinside  32316  btwnconn1lem3  32321  btwnconn1lem4  32322  btwnconn1lem14  32332  btwnconn2  32334  btwnconn3  32335  midofsegid  32336  btwnoutside  32357  outsideoftr  32361  lineunray  32379  lineelsb2  32380  itg2addnclem  33591  cnres2  33692  heibor  33750  lsmcv2  34634  lcvat  34635  lcvexchlem4  34642  lcvexchlem5  34643  lfladd  34671  lflsub  34672  lflmul  34673  lshpkrlem4  34718  latm4  34838  omlmod1i2N  34865  cvlsupr7  34953  cvlsupr8  34954  hlatj4  34978  hlrelat3  35016  cvrval3  35017  atcvrj1  35035  atlelt  35042  2atlt  35043  2atjm  35049  3noncolr2  35053  athgt  35060  3dimlem2  35063  3dimlem4OLDN  35069  1cvratex  35077  ps-1  35081  ps-2  35082  hlatexch3N  35084  llnle  35122  atcvrlln2  35123  atcvrlln  35124  lplni2  35141  lplnle  35144  lplnnle2at  35145  lplnnlelln  35147  llncvrlpln2  35161  2llnmeqat  35175  lvolnle3at  35186  lvolnlelln  35188  4atlem0ae  35198  lneq2at  35382  lnjatN  35384  lncvrat  35386  2lnat  35388  elpaddri  35406  paddasslem2  35425  padd4N  35444  hlmod1i  35460  llnexchb2  35473  dalawlem2  35476  pclfinN  35504  pexmidlem4N  35577  pl42lem1N  35583  lhp2lt  35605  lhpexle1  35612  lhpexle2lem  35613  lhpj1  35626  lhpmcvr5N  35631  lhp2at0  35636  lhp2at0nle  35639  lhple  35646  lhpat  35647  lhpat4N  35648  4atexlemnslpq  35660  4atexlem7  35679  ltrn11  35730  ltrnle  35733  ltrnm  35735  ltrnj  35736  ltrncvr  35737  ltrnel  35743  ltrncnvel  35746  ltrncnv  35750  ltrnmwOLD  35756  trlat  35774  trl0  35775  trlnidat  35778  trlnid  35784  ltrnatlw  35788  trlne  35790  trlval4  35793  cdlemc5  35800  cdlemd2  35804  cdlemd7  35809  cdlemd8  35810  cdlemd9  35811  cdleme0c  35818  cdleme0e  35822  cdleme0fN  35823  cdleme3g  35839  cdleme3h  35840  cdleme5  35845  cdleme11c  35866  cdleme11h  35871  cdleme11j  35872  cdleme11k  35873  cdleme0nex  35895  cdleme18a  35896  cdleme22gb  35899  cdleme20zN  35906  cdleme20c  35916  cdleme20k  35924  cdleme21a  35930  cdleme21b  35931  cdleme21c  35932  cdleme21ct  35934  cdleme21h  35939  cdleme22d  35948  cdleme22f  35951  cdleme26ee  35965  cdleme30a  35983  cdlemefs45eN  36036  cdleme36a  36065  cdleme36m  36066  cdleme39a  36070  cdleme42b  36083  cdleme43dN  36097  cdlemeg47rv2  36115  cdlemeg46sfg  36125  cdlemeg46rjgN  36127  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemeg46gfv  36135  cdleme48d  36140  cdleme50ltrn  36162  cdlemf1  36166  cdlemf  36168  cdlemg2dN  36195  cdlemg2fvlem  36199  cdlemg2l  36208  cdlemg7fvbwN  36212  cdlemg7aN  36230  cdlemg10c  36244  cdlemg17a  36266  cdlemg17dALTN  36269  cdlemg18a  36283  cdlemg18b  36284  cdlemg31b0a  36300  cdlemg31a  36302  cdlemg31b  36303  ltrnco  36324  cdlemg48  36342  tgrpov  36353  tendoco2  36373  tendoplco2  36384  cdlemh1  36420  cdlemk1  36436  cdlemk26b-3  36510  cdlemk27-3  36512  cdlemk28-3  36513  cdlemk34  36515  cdlemkfid1N  36526  cdlemkid3N  36538  cdlemkid4  36539  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk51  36558  tendospcanN  36629  cdlemm10N  36724  dicvaddcl  36796  dicvscacl  36797  cdlemn6  36808  dihvalcq2  36853  dihord6b  36866  dihord5apre  36868  dihglbcpreN  36906  dihjatc1  36917  dihmeetlem20N  36932  dih1dimatlem0  36934  dihglblem6  36946  dochexmidlem4  37069  mapdpglem32  37311  mapdh8ad  37385  mapdh9aOLDN  37397  hdmap11lem2  37451  hdmap14lem6  37482  mzpmfp  37627  mzpsubst  37628  pellex  37716  pellfundex  37767  pellfund14gap  37768  qirropth  37790  rmxypos  37831  congmul  37851  congsub  37854  mzpcong  37856  coprmdvdsb  37869  jm2.15nn0  37887  jm2.16nn0  37888  rpnnen3lem  37915  idomsubgmo  38093  relexp01min  38322  mullimc  40166  islptre  40169  mullimcf  40173  addlimc  40198  0ellimcdiv  40199  limsupre3lem  40282  limsupre3uzlem  40285  fourierdlem48  40689  fourierdlem80  40721  opnvonmbllem2  41168  ovolval5lem3  41189  ovnovollem3  41193  lincfsuppcl  42527  lindslinindimp2lem3  42574
  Copyright terms: Public domain W3C validator