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

Theorem simpr2 1243
Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpr2 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜒)

Proof of Theorem simpr2
StepHypRef Expression
1 simpr 473 . 2 ((𝜑𝜒) → 𝜒)
213ad2antr2 1233 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simplr2OLD  1271  simprr2OLD  1283  simpr12  1342  simpr22  1348  simpr32  1354  simp1r2  1362  simp2r2  1368  simp3r2  1374  3anandis  1588  fpr2g  6700  isopolem  6819  fr3nr  7209  frfi  8444  intrnfi  8561  fisupcl  8614  cnfcomlem  8843  ackbij1lem15  9341  cofsmo  9376  sornom  9384  fpwwe2lem5  9741  dedekindle  10486  supmul1  11277  eluzuzle  11913  xlesubadd  12311  elioc2  12454  elico2  12455  elicc2  12456  fseq1p1m1  12637  fz0fzelfz0  12669  swrdsbslen  13672  swrdspsleq  13673  ccatswrd  13680  swrdswrdlem  13683  tanadd  15117  dvds2ln  15237  cshwsidrepsw  16012  ressress  16150  f1ovscpbl  16391  mreexexlem4d  16512  mreexexd  16513  iscatd2  16546  2oppccomf  16589  issubc3  16713  fthmon  16791  fuccocl  16828  fucidcl  16829  invfuc  16838  initoeu2lem0  16867  initoeu2lem1  16868  curf2cl  17076  yonedalem4c  17122  yonedalem3  17125  pospo  17178  latjle12  17267  latjlej1  17270  latnlej2  17276  latlem12  17283  latmlem1  17286  latledi  17294  latjass  17300  latj12  17301  latj32  17302  latj13  17303  latj31  17304  latjrot  17305  latjjdi  17308  latjjdir  17309  latdisdlem  17394  prdsmndd  17528  frmdmnd  17601  grpsubrcan  17701  grpsubadd  17708  grpaddsubass  17710  grpsubsub4  17713  grppnpcan2  17714  grpnpncan  17715  mulgnndir  17773  mulgnn0dir  17774  mulgdir  17776  mulgnnass  17779  mulgnn0ass  17780  mulgass  17781  mulgsubdir  17784  pwsmulg  17789  issubg2  17811  eqgval  17845  qusgrp  17851  galcan  17938  gacan  17939  oppgmnd  17985  symggrp  18021  fvcosymgeq  18050  pmtrprfv  18074  psgnunilem3  18117  cmn32  18412  cmn12  18414  abladdsub  18421  ablsubsub23  18431  mulgdi  18433  mulgsubdi  18436  dprdss  18630  dprdz  18631  dprdf1o  18633  dprdsn  18637  dprd2da  18643  dmdprdsplit  18648  ablfac1b  18671  pgpfac1lem5  18680  srgi  18713  srgbinom  18747  ringi  18762  prdsringd  18814  opprring  18833  mulgass3  18839  dvrass  18892  subrgunit  19002  issubrg2  19004  abvdiv  19041  lsssn0  19152  islss3  19166  prdslmodd  19176  islmhm2  19245  lspsolv  19351  islbs2  19363  islbs3  19364  lbsextlem4  19370  sralmod  19396  issubassa  19533  sraassa  19534  psrbaglesupp  19577  psrbaglecl  19578  psrbagcon  19580  psrgrp  19607  psrlmod  19610  psrring  19620  psrassa  19623  psgndiflemB  20154  ipdir  20194  ipdi  20195  ipsubdir  20197  ipsubdi  20198  ipass  20200  ipassr  20201  ipassr2  20202  isphld  20209  ocvlss  20226  mamudm  20404  matring  20459  matassa  20460  ofco2  20468  ma1repveval  20588  mdetunilem1  20629  mdetunilem9  20637  chpscmatgsumbin  20862  iinopn  20920  restopnb  21193  subbascn  21272  nrmsep2  21374  isnrm3  21377  regsep2  21394  dnsconst  21396  dfconn2  21436  1stcelcls  21478  dislly  21514  ptuni2  21593  tx1stc  21667  0nelfb  21848  infil  21880  fsubbas  21884  filssufilg  21928  hauspwpwf1  22004  cnextcn  22084  tmdcn2  22106  ustuqtoplem  22256  utopsnneiplem  22264  psmettri  22329  isxmet2d  22345  xmettri  22369  xmetres2  22379  bldisj  22416  blss2ps  22421  blss2  22422  xmstri2  22484  mstri2  22485  xmstri  22486  mstri  22487  xmstri3  22488  mstri3  22489  msrtri  22490  comet  22531  stdbdbl  22535  met2ndci  22540  ngprcan  22627  ngplcan  22628  ngpsubcan  22631  nmtri2  22644  nrgdsdi  22682  nrgdsdir  22683  nlmdsdi  22698  nlmdsdir  22699  blcvx  22814  icoopnst  22951  pi1grplem  23061  clmpm1dir  23115  cmodscmulexp  23134  cvsdiv  23144  cvsdivcl  23145  cphdivcl  23194  cphsubdir  23220  cphsubdi  23221  tchcph  23248  bcthlem5  23337  volfiniun  23528  volcn  23587  itg1val2  23665  dvconst  23894  dvlip  23970  ftc1a  24014  ulmval  24348  ulmdvlem3  24370  ang180  24758  cvxcl  24925  scvxcvx  24926  sgmmul  25140  dchrabl  25193  gausslemma2dlem1a  25304  motgrp  25652  iscgra1  25916  cgrane1  25918  cgrane3  25920  cgrahl1  25922  cgrahl2  25923  cgracgr  25924  cgratr  25929  cgrabtwn  25931  cgrahl  25932  dfcgra2  25935  sacgr  25936  f1otrge  25966  colinearalglem1  26000  axcgrtr  26009  axeuclidlem  26056  axcontlem3  26060  axcontlem4  26061  axcontlem7  26064  eengtrkg  26079  eengtrkge  26080  edglnl  26253  subgruhgredgd  26392  nbfusgrlevtxm2  26496  lfgriswlk  26813  wwlknbp1  26965  umgrwwlks2on  27098  rusgrnumwwlks  27116  clwlkclwwlkfo  27152  3spthd  27349  3vfriswmgr  27453  frgr2wwlkeqm  27506  numclwwlk1lem2f  27534  numclwwlk2  27561  numclwwlk2OLD  27568  numclwwlk3  27573  numclwwlk5  27576  grpomuldivass  27724  ablomuldiv  27735  ablodivdiv4  27737  ablonnncan1  27740  nvmdi  27831  dipassr  28029  archiabllem2c  30074  dvrdir  30115  dvrcan5  30118  reofld  30165  pstmfval  30264  qqhval2lem  30350  qqhvq  30356  measdivcstOLD  30612  measdivcst  30613  carsggect  30705  tgoldbachgtd  31065  bnj1098  31177  bnj149  31268  bnj1118  31375  erdszelem9  31504  resconn  31551  cvmseu  31581  cvmlift2lem10  31617  cvmlift2lem12  31619  elmrsubrn  31740  mclsind  31790  noprefixmo  32169  nosupbnd1  32181  ssltss2  32225  cgrid2  32431  segconeu  32439  btwncomim  32441  btwnswapid  32445  trisegint  32456  cgrxfr  32483  brofs2  32505  endofsegid  32513  btwnconn2  32530  seglemin  32541  segletr  32542  btwnsegle  32545  colinbtwnle  32546  broutsideof2  32550  btwnoutside  32553  broutsideof3  32554  outsideoftr  32557  outsidele  32560  fvray  32569  fvline  32572  ellines  32580  broucube  33756  ftc1anc  33805  sdclem1  33850  sstotbnd2  33884  iscringd  34108  lsmsat  34788  lfladdcl  34851  lflnegcl  34855  lflvscl  34857  eqlkr  34879  lshpkrlem4  34893  lshpkrlem6  34895  ldualgrplem  34925  lduallmodlem  34932  latmassOLD  35009  latm12  35010  latm32  35011  latmrot  35012  latmmdiN  35014  latmmdir  35015  omlfh1N  35038  omlfh3N  35039  cvrnbtwn2  35055  cvlexchb1  35110  cvlsupr2  35123  hlatjass  35150  hlatj12  35151  hlatj32  35152  cvrat  35202  cvrat2  35209  atltcvr  35215  atexchltN  35221  cvrat3  35222  cvrat4  35223  atbtwnexOLDN  35227  atbtwnex  35228  3dimlem3  35241  3dimlem3OLDN  35242  3at  35270  2atneat  35295  llncmp  35302  2at0mat0  35305  2atmat0  35306  llncvrlpln  35338  lplncmp  35342  2llnjaN  35346  4atlem11  35389  lplncvrlvol  35396  lvolcmp  35397  2atm2atN  35565  elpaddatriN  35583  paddasslem8  35607  paddass  35618  padd12N  35619  paddssw2  35624  paddss  35625  pmod1i  35628  pmodN  35630  pmapjlln1  35635  atmod1i1  35637  atmod1i2  35639  pexmidlem2N  35751  pl42lem2N  35760  pl42lem3N  35761  pl42lem4N  35762  pl42N  35763  lhpm0atN  35809  lautlt  35871  lautcvr  35872  lautj  35873  lautm  35874  ltrneq2  35928  cdlemd1  35979  cdleme1b  36007  cdleme1  36008  cdleme2  36009  cdleme3e  36013  cdlemefr27cl  36184  cdlemefs27cl  36194  cdleme42ke  36266  cdleme42mN  36268  cdlemf2  36343  cdlemftr2  36347  trljco  36521  tgrpgrplem  36530  tendoplass  36564  tendodi1  36565  tendodi2  36566  cdlemk34  36691  cdlemk36  36694  erngdvlem3-rN  36779  tendospdi1  36801  dialss  36827  dvhvaddass  36878  dvhopvsca  36883  dvhlveclem  36889  diblss  36951  diclss  36974  diclspsn  36975  cdlemn11pre  36991  dihmeetlem12N  37099  dihmeetlem16N  37103  dihmeetlem17N  37104  dihmeetlem18N  37105  dvh4dimN  37228  lpolconN  37268  dochpolN  37271  lclkr  37314  lclkrs  37320  lcfr  37366  irrapxlem6  37893  jm2.26lem3  38069  dgrsub2  38206  mpaaroot  38226  mendring  38263  mendlmod  38264  mendassa  38265  relexpmulg  38502  iunrelexpmin2  38504  relexpxpmin  38509  neicvgel1  38917  rfcnpre3  39686  fmuldfeq  40295  xlimbr  40533  stoweidlem43  40739  stoweidlem52  40748  stoweidlem53  40749  stoweidlem56  40752  stoweidlem57  40753  stoweidlem60  40756  issmfle  41436  issmfgt  41447  issmfge  41460  smflimlem4  41464  ltsubsubaddltsub  41891  iccpartigtl  41934  iccelpart  41944  upgrwlkupwlk  42289  copissgrp  42376  cznrng  42523  funcringcsetcALTV2lem9  42612  funcringcsetclem9ALTV  42635  ldepsprlem  42829  lincresunit3  42838  lincreslvec3  42839
  Copyright terms: Public domain W3C validator