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

Theorem simplrr 777
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplrr (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜒)

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 486 . 2 ((𝜓𝜒) → 𝜒)
21ad2antlr 726 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  disjxiun  5107  frpomin  6299  fsnex  7234  f1prex  7235  isotr  7286  weniso  7304  riota5f  7347  frxp2  8081  frxp3  8088  xpord3pred  8089  poseq  8095  fprlem2  8237  tfrlem9a  8337  oaass  8513  oeeui  8554  oaabs2  8600  coflton  8622  cofon1  8623  naddssim  8636  resixpfo  8881  omxpenlem  9024  pw2f1olem  9027  fopwdom  9031  fofinf1o  9278  marypha1lem  9376  ordiso2  9458  oismo  9483  ixpiunwdom  9533  cantnf  9636  ttrclss  9663  fseqenlem1  9967  iunfictbso  10057  dfac12lem2  10087  dfac12lem3  10088  infunsdom1  10156  infpssrlem5  10250  fin23lem24  10265  isf32lem2  10297  isf32lem4  10299  isf34lem4  10320  fin1a2lem12  10354  fin1a2lem13  10355  ttukeylem6  10457  fpwwe2lem11  10584  fpwwe2lem12  10585  fpwwe2  10586  winalim2  10639  wunex2  10681  tskord  10723  prlem934  10976  mulcmpblnr  11014  dedekind  11325  addid1  11342  cnegex  11343  negeu  11398  add20  11674  divdivdiv  11863  ltmul12a  12018  lemul12a  12020  lediv12a  12055  supaddc  12129  supmul1  12131  cru  12152  uzwo3  12875  xleadd1a  13179  xmullem  13190  xmulgt0  13209  xlemul1a  13214  ixxun  13287  ixxss12  13291  ioodisj  13406  fz0fzelfz0  13554  mulexpz  14015  rpexpmord  14080  leexp1a  14087  expmulnbnd  14145  hashf1  14363  fi1uzind  14403  brfi1indALT  14406  swrdccat  14630  reuccatpfxs1  14642  abs3lem  15230  rexanre  15238  cau3lem  15246  limsupgre  15370  limsupbnd2  15372  o1lo1  15426  rlimclim1  15434  rlimclim  15435  rlimcn1  15477  rlimcn3  15479  o1of2  15502  o1rlimmul  15508  lo1add  15516  lo1mul  15517  isercolllem1  15556  climcau  15562  caucvgrlem  15564  caucvgb  15571  summolem2  15608  summo  15609  modfsummod  15686  o1fsum  15705  prodmolem2  15825  addmodlteqALT  16214  rpdvds  16543  isprm5  16590  isprm6  16597  pclem  16717  pcqmul  16732  pcexp  16738  pcneg  16753  pcprmpw2  16761  pcadd  16768  pcmpt  16771  4sqlem13  16836  vdwlem2  16861  vdwlem7  16866  vdwlem12  16871  ramval  16887  ramub2  16893  ramz2  16903  ramcl  16908  cshwshashlem2  16976  imasval  17400  imasdsval  17404  mreexexd  17535  acsfn  17546  issubc3  17742  idfucl  17774  funcres2c  17795  isnat  17841  fucpropd  17873  xpcval  18072  xpcco  18078  prfval  18094  evlf2  18114  evlfcl  18118  curf12  18123  curf1cl  18124  curf2  18125  curfcl  18128  curf2ndf  18143  hof2val  18152  hofcl  18155  hofpropd  18163  yonedalem4a  18171  yonedainv  18177  drsdirfi  18201  pospo  18241  poslubmo  18307  posglbmo  18308  isipodrs  18433  acsinfd  18452  gsumvalx  18538  gsumpropd2lem  18541  ismndd  18585  mndpropd  18588  mhmeql  18643  mndind  18645  frmdup3lem  18683  mhmmnd  18876  issubg4  18954  ssnmz  18975  conjnmzb  19050  f1otrspeq  19236  psgneu  19295  pgpfi  19394  sylow2blem3  19411  slwhash  19413  fislw  19414  sylow3lem2  19417  lsmdisj2  19471  pj1eu  19485  efgredlem  19536  frgpuplem  19561  gexex  19638  frgpnabl  19660  dprdfadd  19806  dpjidcl  19844  pgpfac1lem3  19863  pgpfaclem3  19869  ablfac2  19875  ablsimpgcygd  19892  ablsimpgfind  19896  ablsimpgprmd  19901  ringpropd  20013  islmhm2  20515  lmhmpropd  20550  lbsextlem4  20638  prmirredlem  20909  psgndiflemA  21021  lsmcss  21112  uvcf1  21214  frlmsslsp  21218  frlmup1  21220  assapropd  21291  psrval  21333  evlslem1  21508  mamucl  21764  mamuass  21765  mamudi  21766  mamudir  21767  mamuvs1  21768  mamuvs2  21769  mamulid  21806  mamurid  21807  dmatsubcl  21863  dmatmulcl  21865  scmatscm  21878  marrepval  21927  marepveval  21933  mdetunilem7  21983  gsummatr01lem4  22023  cpmatmcllem  22083  mat2pmatf1  22094  mat2pmatlin  22100  decpmatmul  22137  pm2mpmhmlem2  22184  chpidmat  22212  pptbas  22374  toponmre  22460  restbas  22525  iscncl  22636  cnrest2  22653  cnpdis  22660  lmcnp  22671  dishaus  22749  cmpcovf  22758  tgcmp  22768  dfconn2  22786  clsconn  22797  2ndcctbss  22822  dis2ndc  22827  1stccnp  22829  islly2  22851  cldllycmp  22862  locfincmp  22893  comppfsc  22899  kgentopon  22905  txcls  22971  ptpjopn  22979  dfac14  22985  xkoccn  22986  txcnp  22987  txcmpb  23011  txlm  23015  xkopt  23022  xkoco1cn  23024  xkoco2cn  23025  qtopcn  23081  qtoprest  23084  regr1lem2  23107  xkocnv  23181  qtophmeo  23184  fmfnfmlem4  23324  hausflim  23348  hauspwpwf1  23354  fclscmp  23397  alexsublem  23411  alexsubALTlem2  23415  alexsubALTlem3  23416  ptcmplem3  23421  ptcmplem4  23422  ptcmplem5  23423  cnextfun  23431  tmdgsum2  23463  symgtgp  23473  tsmsval2  23497  tsmsgsum  23506  utoptop  23602  ismet2  23702  blin  23790  metss2lem  23883  methaus  23892  met1stc  23893  met2ndci  23894  prdsxmslem2  23901  metcnp3  23912  metcnpi3  23918  metustto  23925  metustfbas  23929  nlmvscn  24067  nrginvrcn  24072  xrsxmet  24188  reconnlem1  24205  reconn  24207  xrge0tsms  24213  xmetdcn2  24216  metdscn  24235  addcnlem  24243  fsumcn  24249  cnheiborlem  24333  cnheibor  24334  bndth  24337  lebnum  24343  nmoleub2lem2  24495  ipcn  24626  iscmet3  24673  caubl  24688  rrxdstprj1  24789  minveclem3b  24808  minveclem7  24815  pjthlem2  24818  pmltpc  24830  volfiniun  24927  ioombl1  24942  dyadss  24974  dyaddisjlem  24975  dyadmax  24978  dyadmbllem  24979  opnmbllem  24981  itg1addlem2  25077  itg10a  25091  mbfi1fseqlem6  25101  itg2seq  25123  itg2monolem1  25131  itg2gt0  25141  itgfsum  25207  limcfval  25252  ellimc2  25257  ellimc3  25259  limcres  25266  limciun  25274  dvres  25291  dveflem  25359  rolle  25370  dvlip2  25375  c1liplem1  25376  dvgt0lem1  25382  dvgt0  25384  dvlt0  25385  dvne0  25391  dvfsumrlimge0  25410  ftc1lem6  25421  itgsubst  25429  mdegmullem  25459  ply1domn  25504  ply1divex  25517  fta1g  25548  fta1b  25550  plyf  25575  dgrlem  25606  coeid  25615  plydivalg  25675  aannenlem1  25704  aalioulem3  25710  aalioulem6  25713  abelthlem8  25814  efif1olem4  25917  chordthm  26203  xrlimcnp  26334  jensen  26354  lgamcvglem  26405  lgamcvg2  26420  sqf11  26504  fsumvma2  26578  perfectlem2  26594  lgsdilem  26688  lgsquad2lem2  26749  lgsquad3  26751  2sqlem5  26786  2sqlem9  26791  2sqb  26796  rpvmasumlem  26851  dchrisum0flb  26874  dchrisum0  26884  pntpbnd  26952  pntibndlem3  26956  pntleml  26975  nolt02o  27059  nosupbday  27069  nosupbnd2  27080  noinfbday  27084  noinfbnd2  27095  noetasuplem4  27100  noetainflem4  27104  noetalem1  27105  conway  27160  slerec  27180  sltlpss  27258  addsprop  27310  mulsproplem10  27410  tgjustc1  27459  tgjustc2  27460  legov  27569  legtrid  27575  tglinethru  27620  tglnpt2  27625  tglineintmo  27626  mirreu3  27638  perpcom  27697  colperpexlem3  27716  mideu  27722  opphllem1  27731  hlpasch  27740  lnopp2hpgb  27747  trgcopy  27788  brcgr  27891  brbtwn2  27896  colinearalg  27901  axsegcon  27918  axeuclidlem  27953  axcontlem9  27963  ecgrtg  27974  elntg  27975  eengtrkg  27977  upgr1eopALT  28110  usgredg4  28207  subuhgr  28276  subumgr  28278  usgr2wspthon  28952  clwlkclwwlkf1  28996  eupth2lems  29224  n4cyclfrgr  29277  vacn  29678  blocni  29789  ubthlem3  29856  minvecolem7  29867  chocunii  30285  pjhthmo  30286  pjhthlem2  30376  kbass5  31104  mdsymlem5  31391  foresf1o  31473  fcobij  31681  xrofsup  31714  mgcoval  31888  mgcf1o  31905  xrge0tsmsd  31941  symgcntz  31978  archirngz  32067  archiabllem2a  32072  isarchiofld  32152  prmidl2  32253  smatrcl  32417  reff  32460  ordtconnlem1  32545  qqhval2  32603  volmeas  32870  fiunelcarsg  32956  ballotlemfc0  33132  ballotlemfcc  33133  signstfvneq0  33224  derangenlem  33805  erdsze2lem1  33837  pconnconn  33865  connpconn  33869  cvxsconn  33877  cvmliftmolem2  33916  cvmliftmo  33918  cvmlift2lem10  33946  cvmlift2lem12  33948  cvmlift3lem7  33959  mrsubff1  34148  msubff1  34190  ifscgr  34658  cgrxfr  34669  btwnconn1lem13  34713  btwnconn1lem14  34714  outsideofeq  34744  ellines  34766  finminlem  34819  fnejoin2  34870  unbdqndv2  35003  irrdiff  35826  poimirlem13  36120  poimirlem14  36121  poimirlem32  36139  opnmbllem0  36143  mblfinlem3  36146  itg2addnclem  36158  itg2addnc  36161  ftc1cnnc  36179  upixp  36217  filbcmb  36228  sstotbnd2  36262  isbnd3  36272  prdsbnd2  36283  cntotbnd  36284  ismtyima  36291  bfp  36312  rrncmslem  36320  unichnidl  36519  lshpcmp  37479  islshpat  37508  lfl0f  37560  ishlat3N  37845  3dim1  37959  islvol5  38071  lvoli2  38073  lncvrelatN  38273  pclfinclN  38442  pexmidlem8N  38469  idltrn  38642  cdleme42keg  38978  cdleme42mgN  38980  cdlemf2  39054  cdlemg2cex  39083  trlcoat  39215  dihopelvalcpre  39740  dih1dimatlem  39821  dihjatcclem4  39913  lcfl7N  39993  lcfrlem9  40042  mapdh9a  40281  hdmapglem7  40421  aks4d1p8  40573  sticksstones11  40593  imacrhmcl  40724  imadrhmcl  40745  fsuppind  40794  fsuppssind  40797  mhpind  40798  mhphf  40800  renegeulemv  40866  sn-subeu  40924  remulinvcom  40930  itrere  40964  retire  40965  prjspertr  40972  prjspreln0  40976  flt4lem7  41026  nna4b4nsq  41027  nacsfix  41064  mzpsubst  41100  mzpcompact2lem  41103  eldioph2lem2  41113  eldioph2  41114  eldioph2b  41115  diophin  41124  diophun  41125  irrapxlem3  41176  irrapxlem5  41178  pell1234qrreccl  41206  pell1234qrmulcl  41207  pell14qrdich  41221  pell1qrge1  41222  pell1qrgaplem  41225  monotuz  41294  acongtr  41331  acongrep  41333  jm2.23  41349  jm2.26a  41353  jm2.26lem3  41354  jm2.26  41355  jm2.27  41361  wepwsolem  41398  fnwe2lem2  41407  kelac1  41419  kercvrlsm  41439  hbtlem5  41484  hbt  41486  mpaaeu  41506  cantnfresb  41688  onmcl  41695  naddcnff  41707  rfovcnvf1od  42350  mnurndlem1  42635  cncmpmax  43311  rfcnnnub  43315  disjxp1  43351  iccintsng  43835  fprodcn  43915  lptioo2  43946  lptioo1  43947  limclner  43966  stoweidlem31  44346  stoweidlem34  44349  stoweidlem35  44350  stoweidlem49  44364  stoweidlem59  44374  stoweidlem62  44377  fourierdlem60  44481  fourierdlem61  44482  fourierdlem87  44508  iundjiun  44775  ismeannd  44782  hoidmvle  44915  smfsuplem2  45127  2reu8i  45419  prproropf1olem2  45770  paireqne  45777  perfectALTVlem2  45988  mogoldbb  46051  bgoldbtbndlem2  46072  bgoldbtbndlem3  46073  isomgrtrlem  46104  mgmhmeql  46171  mndpsuppss  46521  scmsuppss  46522  lindslinindsimp2lem5  46617  elfzolborelfzop1  46674  elbigolo1  46717  itschlc0xyqsol1  46926  itschlc0xyqsol  46927  iccdisj  47005  toslat  47081  functhinclem4  47138
  Copyright terms: Public domain W3C validator