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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 472 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 763 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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
This theorem is referenced by:  disjxiun  4681  disjxiunOLD  4682  f1imass  6561  f1prex  6579  soisoi  6618  riota5f  6676  tfrlem9a  7527  oeeui  7727  oaabs2  7770  omabs  7772  omxpenlem  8102  fopwdom  8109  frfi  8246  marypha1lem  8380  ordiso2  8461  oismo  8486  wemaplem3  8494  cantnf  8628  isinffi  8856  dfac12lem2  9004  dfac12lem3  9005  infxp  9075  infmap2  9078  infpssrlem5  9167  fin23lem11  9177  fin23lem24  9182  fin23lem26  9185  isf32lem2  9214  isf32lem4  9216  fin1a2lem13  9272  fin1a2s  9274  ttukeylem5  9373  fpwwe2lem12  9501  fpwwe2lem13  9502  wunex2  9598  tskord  9640  prlem934  9893  mulcmpblnr  9930  dedekind  10238  addid1  10254  cnegex  10255  negeu  10309  add20  10578  divdivdiv  10764  ltmul12a  10917  lediv12a  10954  cru  11050  uzwo3  11821  xleadd1a  12121  xlemul1a  12156  ixxun  12229  ixxss12  12233  elfz0ubfz0  12482  mulexpz  12940  leexp1a  12959  expmulnbnd  13036  swrdccat3  13538  abs3lem  14122  rexanre  14130  cau3lem  14138  lo1bdd2  14299  o1lo1  14312  rlimclim1  14320  rlimclim  14321  lo1resb  14339  o1resb  14341  rlimcn2  14365  o1of2  14387  o1rlimmul  14393  lo1add  14401  lo1mul  14402  isercolllem1  14439  climcau  14445  summolem2  14491  summo  14492  o1fsum  14589  prodmolem2  14709  qredeu  15419  isprm5  15466  pclem  15590  pcqmul  15605  pcexp  15611  pcneg  15625  pcprmpw2  15633  pcadd  15640  prmpwdvds  15655  4sqlem13  15708  vdwlem2  15733  vdwlem7  15738  vdwlem11  15742  vdwlem12  15743  ramval  15759  ramz2  15775  ramcl  15780  prmgaplem6  15807  cshwshashlem2  15850  imasval  16218  imasdsval  16222  mreexexd  16355  mreexexdOLD  16356  issubc3  16556  idfucl  16588  funcres2c  16608  fucpropd  16684  xpcval  16864  prfval  16886  evlfcl  16909  curf12  16914  curf1cl  16915  curf2  16916  curfcl  16919  curfuncf  16925  curf2ndf  16934  hof2val  16943  hofcl  16946  hofpropd  16954  yonedalem4a  16962  yonedainv  16968  poslubmo  17193  posglbmo  17194  isipodrs  17208  acsmapd  17225  acsinfd  17227  ismndd  17360  mndpropd  17363  mhmeql  17411  mrcmndind  17413  frmdup3lem  17450  mhmmnd  17584  issubg4  17660  ssnmz  17683  f1otrspeq  17913  psgneu  17972  sylow2blem3  18083  lsmdisj2  18141  pj1eu  18155  efgredlem  18206  frgpuplem  18231  frgpnabl  18324  dmdprdsplitlem  18482  pgpfac1lem3  18522  pgpfaclem3  18528  ringpropd  18628  dvdsrtr  18698  islmhm2  19086  lmhmpropd  19121  assapropd  19375  evlslem1  19563  coe1tmmul2  19694  prmirredlem  19889  psgndiflemA  19995  lsmcss  20084  dsmmlss  20136  uvcf1  20179  frlmup1  20185  mamucl  20255  mamuass  20256  mamudi  20257  mamudir  20258  mamuvs1  20259  mamuvs2  20260  mamulid  20295  mamurid  20296  dmatsubcl  20352  dmatmulcl  20354  mdetunilem7  20472  mdetunilem9  20474  cramer0  20544  cpmatmcllem  20571  mat2pmatf1  20582  decpmatmul  20625  pmatcollpw1  20629  pm2mpf1lem  20647  pm2mpmhmlem2  20672  chpidmat  20700  cpmadugsumlemB  20727  cpmadugsumlemC  20728  toponmre  20945  restbas  21010  iscncl  21121  cnpdis  21145  lmcnp  21156  dishaus  21234  cmpcovf  21242  hauscmplem  21257  dfconn2  21270  clsconn  21281  2ndcctbss  21306  1stccnp  21313  islly2  21335  llyidm  21339  cldllycmp  21346  locfincmp  21377  kgentopon  21389  1stckgenlem  21404  ptpjpre1  21422  ptbasfi  21432  txcls  21455  ptpjopn  21463  xkoccn  21470  txcnp  21471  txcmpb  21495  xkoptsub  21505  xkoco2cn  21509  xkoinjcn  21538  qtopcn  21565  qtoprest  21568  regr1lem  21590  regr1lem2  21591  kqreglem1  21592  qtophmeo  21668  fgabs  21730  hauspwpwf1  21838  flimfnfcls  21879  fclscmp  21881  cnpfcf  21892  ptcmplem4  21906  ptcmplem5  21907  cnextfval  21913  cnextfun  21915  tmdgsum2  21947  tsmsval2  21980  utoptop  22085  utop3cls  22102  ismet2  22185  blin  22273  metss2lem  22363  methaus  22372  met1stc  22373  met2ndci  22374  metcnp  22393  metcnpi3  22398  metustto  22405  metustfbas  22409  nlmvscn  22538  nrginvrcn  22543  nghmcn  22596  xrsxmet  22659  reconnlem1  22676  reconn  22678  xrge0tsms  22684  xmetdcn2  22687  metdscn  22706  addcnlem  22714  mulc1cncf  22755  cncfco  22757  cnheiborlem  22800  cnheibor  22801  nmoleub2lem2  22962  ipcn  23091  iscfil3  23117  cfilfcls  23118  iscmet3  23137  caubl  23152  bcthlem5  23171  rrxdstprj1  23238  minveclem3b  23245  minveclem7  23252  pmltpc  23265  ovolshftlem1  23323  ovolscalem1  23327  ioombl1  23376  uniioombllem6  23402  dyadss  23408  dyaddisjlem  23409  dyadmax  23412  opnmbllem  23415  itg1addlem2  23509  itg2seq  23554  bddmulibl  23650  limcfval  23681  ellimc3  23688  limciun  23703  dveflem  23787  rolle  23798  dvlip2  23803  c1liplem1  23804  dvgt0lem1  23810  dvgt0  23812  dvlt0  23813  dvne0  23819  dvcnvre  23827  dvfsumrlimge0  23838  ftc1lem6  23849  itgsubst  23857  mdegmullem  23883  ply1domn  23928  fta1g  23972  fta1b  23974  dgrlem  24030  coeid  24039  plydivalg  24099  aannenlem1  24128  aalioulem6  24137  ulmcn  24198  mtestbdd  24204  abelthlem8  24238  efif1olem4  24336  chordthm  24609  xrlimcnp  24740  lgamgulmlem5  24804  isppw2  24886  fsumvma2  24984  perfectlem2  25000  lgsdilem  25094  lgsquad2lem2  25155  lgsquad3  25157  2sqlem5  25192  2sqlem9  25197  rpvmasumlem  25221  dchrisum0flb  25244  pntpbnd  25322  pntibndlem3  25326  pntlem3  25343  pntleml  25345  tgbtwnconn1lem3  25514  legtrid  25531  tglinethru  25576  tglnpt2  25581  tglineintmo  25582  mirreu3  25594  perpcom  25653  footex  25658  mideu  25675  opphllem1  25684  lnopp2hpgb  25700  axsegcon  25852  axpasch  25866  axeuclidlem  25887  ecgrtg  25908  elntg  25909  eengtrkg  25910  upgr1eopALT  26057  usgredg4  26154  usgr1eop  26187  usgr1v  26193  subuhgr  26223  subumgr  26225  subusgr  26226  nbuhgr2vtx1edgb  26293  wwlksnext  26856  usgr2wspthon  26932  clwwisshclwwslem  26971  n4cyclfrgr  27271  vacn  27677  ubthlem1  27854  ubthlem3  27856  minvecolem7  27867  chocunii  28288  pjhthmo  28289  pjhthlem2  28379  nmopub2tALT  28896  nmfnleub2  28913  kbass5  29107  mdslmd1lem1  29312  mdslmd1lem2  29313  mdsymlem5  29394  fcobij  29628  xrofsup  29661  archiabllem2a  29876  gsumvsca1  29910  gsumvsca2  29911  xrge0tsmsd  29913  isarchiofld  29945  smatrcl  29990  reff  30034  ordtconnlem1  30098  qqhval2  30154  esumpcvgval  30268  imambfm  30452  ballotlemsf1o  30703  signstfvneq0  30777  pconnconn  31339  connpconn  31343  cvmliftmo  31392  cvmlift2lem10  31420  cvmlift2lem12  31422  cvmlift3lem7  31433  mrsubff1  31537  msubff1  31579  frpomin  31863  noprefixmo  31973  noetalem3  31990  slerec  32048  ifscgr  32276  cgrxfr  32287  btwnconn1lem13  32331  ellines  32384  unblimceq0lem  32622  unbdqndv2  32627  matunitlindflem1  33535  poimirlem4  33543  poimirlem13  33552  poimirlem14  33553  heicant  33574  opnmbllem0  33575  mblfinlem3  33578  itg2addnclem  33591  itg2addnc  33594  ftc1cnnc  33614  sstotbnd  33704  cntotbnd  33725  ismtyima  33732  heibor1lem  33738  heiborlem10  33749  bfp  33753  rrncmslem  33761  islshpsm  34585  lsatcmp  34608  islshpat  34622  lfl0f  34674  iscvlat2N  34929  ishlat3N  34959  3dim1  35071  islvol5  35183  lvoli2  35185  lncvrelatN  35385  lncmp  35387  paddasslem10  35433  pclfinclN  35554  pexmidlem8N  35581  idltrn  35754  cdleme42keg  36091  cdleme42mgN  36093  cdlemf2  36167  cdlemg2cex  36196  trlcoat  36328  tendoex  36580  erngdvlem4  36596  erngdvlem4-rN  36604  dialss  36652  dibglbN  36772  diblss  36776  dihlsscpre  36840  dihglblem2aN  36899  dihglblem4  36903  dihglblem5  36904  dih1dimatlem  36935  dihglblem6  36946  lcfl7N  37107  lcfrlem9  37156  mapdh9a  37396  hdmapglem7  37538  isnacs3  37590  nacsfix  37592  mzpsubst  37628  eldioph2lem2  37641  eldioph2  37642  eldioph2b  37643  diophin  37653  diophun  37654  rencldnfilem  37701  irrapxlem3  37705  irrapxlem5  37707  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell1qrge1  37751  pell1qrgaplem  37754  monotuz  37823  monotoddzzfi  37824  rpexpmord  37830  acongtr  37862  acongrep  37864  jm2.26a  37884  jm2.26lem3  37885  jm2.26  37886  jm2.27b  37890  jm2.27  37892  wepwsolem  37929  fnwe2lem2  37938  hbtlem5  38015  hbt  38017  mpaaeu  38037  rfovcnvf1od  38615  fnchoice  39502  rfcnnnub  39509  disjxp1  39552  ioondisj2  40032  iccintsng  40067  fprodcn  40150  lptioo2  40181  lptioo1  40182  limclner  40201  dvdsn1add  40472  stoweidlem14  40549  stoweidlem27  40562  stoweidlem34  40569  stoweidlem49  40584  stoweidlem56  40591  fourierdlem87  40728  iundjiun  40995  ismeannd  41002  hoidmvle  41135  pfxccat3  41751  perfectALTVlem2  41956  mogoldbb  41998  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  mgmhmeql  42128  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  mndpsuppss  42477  lindslinindsimp2lem5  42576
  Copyright terms: Public domain W3C validator