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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 484 . 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  5103  frpomin  6295  f1imass  7212  f1prex  7231  soisoi  7274  riota5f  7343  frxp3  8084  xpord3pred  8085  tfrlem9a  8333  oeeui  8550  oaabs2  8596  omabs  8598  naddssim  8632  omxpenlem  9020  fopwdom  9027  frfi  9235  marypha1lem  9374  ordiso2  9456  oismo  9481  wemaplem3  9489  cantnf  9634  ttrclss  9661  isinffi  9933  dfac12lem2  10085  dfac12lem3  10086  infxp  10156  infmap2  10159  infpssrlem5  10248  fin23lem11  10258  fin23lem24  10263  fin23lem26  10266  isf32lem2  10295  isf32lem4  10297  fin1a2lem13  10353  fin1a2s  10355  ttukeylem5  10454  fpwwe2lem11  10582  fpwwe2lem12  10583  wunex2  10679  tskord  10721  prlem934  10974  mulcmpblnr  11012  dedekind  11323  addid1  11340  cnegex  11341  negeu  11396  add20  11672  divdivdiv  11861  ltmul12a  12016  lediv12a  12053  cru  12150  uzwo3  12873  xleadd1a  13178  xlemul1a  13213  ixxun  13286  ixxss12  13290  elfz0ubfz0  13551  mulexpz  14014  rpexpmord  14079  leexp1a  14086  expmulnbnd  14144  swrdccatin1  14619  pfxccatin12lem3  14626  pfxccat3  14628  abs3lem  15229  rexanre  15237  cau3lem  15245  lo1bdd2  15412  o1lo1  15425  rlimclim1  15433  rlimclim  15434  lo1resb  15452  o1resb  15454  rlimcn3  15478  o1of2  15501  o1rlimmul  15507  lo1add  15515  lo1mul  15516  isercolllem1  15555  climcau  15561  summolem2  15606  summo  15607  o1fsum  15703  prodmolem2  15823  qredeu  16539  isprm5  16588  pclem  16715  pcqmul  16730  pcexp  16736  pcneg  16751  pcprmpw2  16759  pcadd  16766  prmpwdvds  16781  4sqlem13  16834  vdwlem2  16859  vdwlem7  16864  vdwlem11  16868  vdwlem12  16869  ramval  16885  ramz2  16901  ramcl  16906  prmgaplem6  16933  cshwshashlem2  16974  imasval  17398  imasdsval  17402  mreexexd  17533  issubc3  17740  idfucl  17772  funcres2c  17793  fucpropd  17871  xpcval  18070  prfval  18092  evlfcl  18116  curf12  18121  curf1cl  18122  curf2  18123  curfcl  18126  curfuncf  18132  curf2ndf  18141  hof2val  18150  hofcl  18153  hofpropd  18161  yonedalem4a  18169  yonedainv  18175  poslubmo  18305  posglbmo  18306  isipodrs  18431  acsmapd  18448  acsinfd  18450  ismndd  18583  mndpropd  18586  mhmeql  18641  mndind  18643  frmdup3lem  18681  mhmmnd  18874  issubg4  18952  ssnmz  18973  f1otrspeq  19234  psgneu  19293  sylow2blem3  19409  lsmdisj2  19469  pj1eu  19483  efgredlem  19534  frgpuplem  19559  frgpnabl  19658  dmdprdsplitlem  19821  pgpfac1lem3  19861  pgpfaclem3  19867  ablsimpgcygd  19890  ringpropd  20011  dvdsrtr  20086  islmhm2  20514  lmhmpropd  20549  prmirredlem  20909  psgndiflemA  21021  lsmcss  21112  dsmmlss  21166  uvcf1  21214  frlmup1  21220  assapropd  21291  evlslem1  21508  coe1tmmul2  21663  mamucl  21764  mamuass  21765  mamudi  21766  mamudir  21767  mamuvs1  21768  mamuvs2  21769  mamulid  21806  mamurid  21807  dmatsubcl  21863  dmatmulcl  21865  mdetunilem7  21983  mdetunilem9  21985  cramer0  22055  cpmatmcllem  22083  mat2pmatf1  22094  decpmatmul  22137  pmatcollpw1  22141  pm2mpf1lem  22159  pm2mpmhmlem2  22184  chpidmat  22212  cpmadugsumlemB  22239  cpmadugsumlemC  22240  toponmre  22460  restbas  22525  iscncl  22636  cnpdis  22660  lmcnp  22671  dishaus  22749  cmpcovf  22758  hauscmplem  22773  dfconn2  22786  clsconn  22797  2ndcctbss  22822  1stccnp  22829  islly2  22851  llyidm  22855  cldllycmp  22862  locfincmp  22893  kgentopon  22905  1stckgenlem  22920  ptpjpre1  22938  ptbasfi  22948  txcls  22971  ptpjopn  22979  xkoccn  22986  txcnp  22987  txcmpb  23011  xkoptsub  23021  xkoco2cn  23025  xkoinjcn  23054  qtopcn  23081  qtoprest  23084  regr1lem  23106  regr1lem2  23107  kqreglem1  23108  qtophmeo  23184  fgabs  23246  hauspwpwf1  23354  flimfnfcls  23395  fclscmp  23397  cnpfcf  23408  ptcmplem4  23422  ptcmplem5  23423  cnextfval  23429  cnextfun  23431  tmdgsum2  23463  tsmsval2  23497  utoptop  23602  utop3cls  23619  ismet2  23702  blin  23790  metss2lem  23883  methaus  23892  met1stc  23893  met2ndci  23894  metcnp  23913  metcnpi3  23918  metustto  23925  metustfbas  23929  nlmvscn  24067  nrginvrcn  24072  nghmcn  24125  xrsxmet  24188  reconnlem1  24205  reconn  24207  xrge0tsms  24213  xmetdcn2  24216  metdscn  24235  addcnlem  24243  mulc1cncf  24284  cncfco  24286  cnheiborlem  24333  cnheibor  24334  nmoleub2lem2  24495  ipcn  24626  iscfil3  24653  cfilfcls  24654  iscmet3  24673  caubl  24688  bcthlem5  24708  rrxdstprj1  24789  minveclem3b  24808  minveclem7  24815  pmltpc  24830  ovolshftlem1  24889  ovolscalem1  24893  ioombl1  24942  uniioombllem6  24968  dyadss  24974  dyaddisjlem  24975  dyadmax  24978  opnmbllem  24981  itg1addlem2  25077  itg2seq  25123  bddmulibl  25219  limcfval  25252  ellimc3  25259  limciun  25274  dveflem  25359  rolle  25370  dvlip2  25375  c1liplem1  25376  dvgt0lem1  25382  dvgt0  25384  dvlt0  25385  dvne0  25391  dvcnvre  25399  dvfsumrlimge0  25410  ftc1lem6  25421  itgsubst  25429  mdegmullem  25459  ply1domn  25504  fta1g  25548  fta1b  25550  dgrlem  25606  coeid  25615  plydivalg  25675  aannenlem1  25704  aalioulem6  25713  ulmcn  25774  mtestbdd  25780  abelthlem8  25814  efif1olem4  25917  chordthm  26203  xrlimcnp  26334  lgamgulmlem5  26398  isppw2  26480  fsumvma2  26578  perfectlem2  26594  lgsdilem  26688  lgsquad2lem2  26749  lgsquad3  26751  2sqlem5  26786  2sqlem9  26791  rpvmasumlem  26851  dchrisum0flb  26874  pntpbnd  26952  pntibndlem3  26956  pntlem3  26973  pntleml  26975  nosupbday  27069  noinfbday  27084  noetasuplem4  27100  noetainflem4  27104  noetalem1  27105  slerec  27180  madebdaylemlrcut  27250  mulsproplem10  27410  tgjustc1  27459  tgjustc2  27460  tgbtwnconn1lem3  27558  legtrid  27575  tglinethru  27620  tglnpt2  27625  tglineintmo  27626  mirreu3  27638  perpcom  27697  footexALT  27702  footex  27705  mideu  27722  opphllem1  27731  lnopp2hpgb  27747  axsegcon  27918  axpasch  27932  axeuclidlem  27953  ecgrtg  27974  elntg  27975  eengtrkg  27977  upgr1eopALT  28110  usgredg4  28207  usgr1eop  28240  usgr1v  28246  subuhgr  28276  subumgr  28278  subusgr  28279  nbuhgr2vtx1edgb  28342  wwlksnext  28880  usgr2wspthon  28952  clwlkclwwlkf1  28996  clwwisshclwwslem  29000  n4cyclfrgr  29277  dlwwlknondlwlknonf1o  29351  vacn  29678  ubthlem1  29854  ubthlem3  29856  minvecolem7  29867  chocunii  30285  pjhthmo  30286  pjhthlem2  30376  nmopub2tALT  30893  nmfnleub2  30910  kbass5  31104  mdslmd1lem1  31309  mdslmd1lem2  31310  mdsymlem5  31391  fcobij  31686  xrofsup  31719  mgcf1o  31912  xrge0tsmsd  31948  symgcntz  31985  archiabllem2a  32079  gsumvsca1  32110  gsumvsca2  32111  isarchiofld  32159  prmidl2  32261  ssmxidl  32287  smatrcl  32434  reff  32477  ordtconnlem1  32562  qqhval2  32620  esumpcvgval  32734  imambfm  32919  ballotlemsf1o  33170  signstfvneq0  33241  pconnconn  33882  connpconn  33886  cvmliftmo  33935  cvmlift2lem10  33963  cvmlift2lem12  33965  cvmlift3lem7  33976  mrsubff1  34165  msubff1  34207  ifscgr  34675  cgrxfr  34686  btwnconn1lem13  34730  ellines  34783  unblimceq0lem  35015  unbdqndv2  35020  irrdiff  35843  matunitlindflem1  36120  poimirlem4  36128  poimirlem13  36137  poimirlem14  36138  heicant  36159  opnmbllem0  36160  mblfinlem3  36163  itg2addnclem  36175  itg2addnc  36178  ftc1cnnc  36196  sstotbnd  36280  cntotbnd  36301  ismtyima  36308  heibor1lem  36314  heiborlem10  36325  bfp  36329  rrncmslem  36337  islshpsm  37488  lsatcmp  37511  islshpat  37525  lfl0f  37577  iscvlat2N  37832  ishlat3N  37862  3dim1  37976  islvol5  38088  lvoli2  38090  lncvrelatN  38290  lncmp  38292  paddasslem10  38338  pclfinclN  38459  pexmidlem8N  38486  idltrn  38659  cdleme42keg  38995  cdleme42mgN  38997  cdlemf2  39071  cdlemg2cex  39100  trlcoat  39232  tendoex  39484  erngdvlem4  39500  erngdvlem4-rN  39508  dialss  39555  dibglbN  39675  diblss  39679  dihlsscpre  39743  dihglblem2aN  39802  dihglblem4  39806  dihglblem5  39807  dih1dimatlem  39838  dihglblem6  39849  lcfl7N  40010  lcfrlem9  40059  mapdh9a  40298  hdmapglem7  40438  aks4d1p8  40590  sticksstones22  40622  imacrhmcl  40740  fsuppind  40808  renegeulemv  40880  sn-subeu  40938  remulinvcom  40944  itrere  40978  retire  40979  prjspertr  40986  prjspreln0  40990  flt4lem7  41040  nna4b4nsq  41041  isnacs3  41076  nacsfix  41078  mzpsubst  41114  eldioph2lem2  41127  eldioph2  41128  eldioph2b  41129  diophin  41138  diophun  41139  rencldnfilem  41186  irrapxlem3  41190  irrapxlem5  41192  pell1234qrreccl  41220  pell1234qrmulcl  41221  pell1qrge1  41236  pell1qrgaplem  41239  monotuz  41308  monotoddzzfi  41309  acongtr  41345  acongrep  41347  jm2.26a  41367  jm2.26lem3  41368  jm2.26  41369  jm2.27b  41373  jm2.27  41375  wepwsolem  41412  fnwe2lem2  41421  hbtlem5  41498  hbt  41500  mpaaeu  41520  cantnftermord  41698  cantnfresb  41702  omabs2  41710  naddcnff  41721  oaun3lem1  41733  rfovcnvf1od  42364  mnurndlem1  42649  fnchoice  43322  rfcnnnub  43329  disjxp1  43365  ioondisj2  43817  iccintsng  43847  fprodcn  43927  lptioo2  43958  lptioo1  43959  limclner  43978  dvdsn1add  44266  stoweidlem14  44341  stoweidlem27  44354  stoweidlem34  44361  stoweidlem49  44376  stoweidlem56  44383  fourierdlem87  44520  iundjiun  44787  ismeannd  44794  hoidmvle  44927  prproropf1olem2  45782  perfectALTVlem2  46000  mogoldbb  46063  bgoldbtbndlem2  46084  bgoldbtbndlem3  46085  mgmhmeql  46183  rngcinv  46365  rngcinvALTV  46377  ringcinv  46416  ringcinvALTV  46440  mndpsuppss  46533  lindslinindsimp2lem5  46629  itscnhlinecirc02p  46957  toslat  47093  functhinclem4  47150
  Copyright terms: Public domain W3C validator