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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 481 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 725 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  disjxiun  5142  frpomin  6345  f1imass  7271  f1prex  7290  soisoi  7332  riota5f  7401  frxp3  8157  xpord3pred  8158  tfrlem9a  8408  oeeui  8624  oaabs2  8671  omabs  8673  naddssim  8707  omxpenlem  9103  fopwdom  9110  frfi  9315  marypha1lem  9469  ordiso2  9551  oismo  9576  wemaplem3  9584  cantnf  9729  ttrclss  9756  isinffi  10028  dfac12lem2  10180  dfac12lem3  10181  infxp  10249  infmap2  10252  infpssrlem5  10341  fin23lem11  10351  fin23lem24  10356  fin23lem26  10359  isf32lem2  10388  isf32lem4  10390  fin1a2lem13  10446  fin1a2s  10448  ttukeylem5  10547  fpwwe2lem11  10675  fpwwe2lem12  10676  wunex2  10772  tskord  10814  prlem934  11067  mulcmpblnr  11105  dedekind  11418  addrid  11435  cnegex  11436  negeu  11491  add20  11767  divdivdiv  11960  ltmul12a  12115  lediv12a  12153  cru  12250  uzwo3  12973  xleadd1a  13280  xlemul1a  13315  ixxun  13388  ixxss12  13392  elfz0ubfz0  13653  mulexpz  14116  rpexpmord  14181  leexp1a  14188  expmulnbnd  14247  swrdccatin1  14728  pfxccatin12lem3  14735  pfxccat3  14737  abs3lem  15338  rexanre  15346  cau3lem  15354  lo1bdd2  15521  o1lo1  15534  rlimclim1  15542  rlimclim  15543  lo1resb  15561  o1resb  15563  rlimcn3  15587  o1of2  15610  o1rlimmul  15616  lo1add  15624  lo1mul  15625  isercolllem1  15664  climcau  15670  summolem2  15715  summo  15716  o1fsum  15812  prodmolem2  15932  qredeu  16654  isprm5  16703  pclem  16835  pcqmul  16850  pcexp  16856  pcneg  16871  pcprmpw2  16879  pcadd  16886  prmpwdvds  16901  4sqlem13  16954  vdwlem2  16979  vdwlem7  16984  vdwlem11  16988  vdwlem12  16989  ramval  17005  ramz2  17021  ramcl  17026  prmgaplem6  17053  cshwshashlem2  17094  imasval  17521  imasdsval  17525  mreexexd  17656  issubc3  17863  idfucl  17895  funcres2c  17918  fucpropd  17997  xpcval  18196  prfval  18218  evlfcl  18242  curf12  18247  curf1cl  18248  curf2  18249  curfcl  18252  curfuncf  18258  curf2ndf  18267  hof2val  18276  hofcl  18279  hofpropd  18287  yonedalem4a  18295  yonedainv  18301  poslubmo  18431  posglbmo  18432  isipodrs  18557  acsmapd  18574  acsinfd  18576  mgmhmeql  18704  sgrppropd  18719  ismndd  18744  mndpropd  18747  mhmeql  18811  mndind  18813  frmdup3lem  18851  mhmmnd  19054  issubg4  19135  ssnmz  19156  f1otrspeq  19441  psgneu  19500  sylow2blem3  19616  lsmdisj2  19676  pj1eu  19690  efgredlem  19741  frgpuplem  19766  frgpnabl  19869  dmdprdsplitlem  20033  pgpfac1lem3  20073  pgpfaclem3  20079  ablsimpgcygd  20102  rngpropd  20153  ringpropd  20263  dvdsrtr  20346  rngcinv  20611  ringcinv  20645  islmhm2  21012  lmhmpropd  21047  prmirredlem  21458  psgndiflemA  21593  lsmcss  21684  dsmmlss  21738  uvcf1  21786  frlmup1  21792  assapropd  21865  evlslem1  22093  coe1tmmul2  22263  mamucl  22389  mamuass  22390  mamudi  22391  mamudir  22392  mamuvs1  22393  mamuvs2  22394  mamulid  22431  mamurid  22432  dmatsubcl  22488  dmatmulcl  22490  mdetunilem7  22608  mdetunilem9  22610  cramer0  22680  cpmatmcllem  22708  mat2pmatf1  22719  decpmatmul  22762  pmatcollpw1  22766  pm2mpf1lem  22784  pm2mpmhmlem2  22809  chpidmat  22837  cpmadugsumlemB  22864  cpmadugsumlemC  22865  toponmre  23085  restbas  23150  iscncl  23261  cnpdis  23285  lmcnp  23296  dishaus  23374  cmpcovf  23383  hauscmplem  23398  dfconn2  23411  clsconn  23422  2ndcctbss  23447  1stccnp  23454  islly2  23476  llyidm  23480  cldllycmp  23487  locfincmp  23518  kgentopon  23530  1stckgenlem  23545  ptpjpre1  23563  ptbasfi  23573  txcls  23596  ptpjopn  23604  xkoccn  23611  txcnp  23612  txcmpb  23636  xkoptsub  23646  xkoco2cn  23650  xkoinjcn  23679  qtopcn  23706  qtoprest  23709  regr1lem  23731  regr1lem2  23732  kqreglem1  23733  qtophmeo  23809  fgabs  23871  hauspwpwf1  23979  flimfnfcls  24020  fclscmp  24022  cnpfcf  24033  ptcmplem4  24047  ptcmplem5  24048  cnextfval  24054  cnextfun  24056  tmdgsum2  24088  tsmsval2  24122  utoptop  24227  utop3cls  24244  ismet2  24327  blin  24415  metss2lem  24508  methaus  24517  met1stc  24518  met2ndci  24519  metcnp  24538  metcnpi3  24543  metustto  24550  metustfbas  24554  nlmvscn  24692  nrginvrcn  24697  nghmcn  24750  xrsxmet  24813  reconnlem1  24830  reconn  24832  xrge0tsms  24838  xmetdcn2  24841  metdscn  24860  addcnlem  24868  mulc1cncf  24913  cncfco  24915  cnheiborlem  24968  cnheibor  24969  nmoleub2lem2  25131  ipcn  25262  iscfil3  25289  cfilfcls  25290  iscmet3  25309  caubl  25324  bcthlem5  25344  rrxdstprj1  25425  minveclem3b  25444  minveclem7  25451  pmltpc  25467  ovolshftlem1  25526  ovolscalem1  25530  ioombl1  25579  uniioombllem6  25605  dyadss  25611  dyaddisjlem  25612  dyadmax  25615  opnmbllem  25618  itg1addlem2  25714  itg2seq  25760  bddmulibl  25856  limcfval  25889  ellimc3  25896  limciun  25911  dveflem  25999  rolle  26010  dvlip2  26016  c1liplem1  26017  dvgt0lem1  26023  dvgt0  26025  dvlt0  26026  dvne0  26032  dvcnvre  26040  dvfsumrlimge0  26053  ftc1lem6  26064  itgsubst  26072  mdegmullem  26102  ply1domn  26148  fta1g  26194  fta1b  26196  dgrlem  26253  coeid  26262  plydivalg  26324  aannenlem1  26353  aalioulem6  26362  ulmcn  26425  mtestbdd  26431  abelthlem8  26466  efif1olem4  26569  chordthm  26862  xrlimcnp  26993  lgamgulmlem5  27058  isppw2  27140  fsumvma2  27240  perfectlem2  27256  lgsdilem  27350  lgsquad2lem2  27411  lgsquad3  27413  2sqlem5  27448  2sqlem9  27453  rpvmasumlem  27513  dchrisum0flb  27536  pntpbnd  27614  pntibndlem3  27618  pntlem3  27635  pntleml  27637  nosupbday  27732  noinfbday  27747  noetasuplem4  27763  noetainflem4  27767  noetalem1  27768  slerec  27846  madebdaylemlrcut  27919  remulscllem2  28349  tgjustc1  28399  tgjustc2  28400  tgbtwnconn1lem3  28498  legtrid  28515  tglinethru  28560  tglnpt2  28565  tglineintmo  28566  mirreu3  28578  perpcom  28637  footexALT  28642  footex  28645  mideu  28662  opphllem1  28671  lnopp2hpgb  28687  axsegcon  28858  axpasch  28872  axeuclidlem  28893  ecgrtg  28914  elntg  28915  eengtrkg  28917  upgr1eopALT  29050  usgredg4  29150  usgr1eop  29183  usgr1v  29189  subuhgr  29219  subumgr  29221  subusgr  29222  nbuhgr2vtx1edgb  29285  wwlksnext  29824  usgr2wspthon  29896  clwlkclwwlkf1  29940  clwwisshclwwslem  29944  n4cyclfrgr  30221  dlwwlknondlwlknonf1o  30295  vacn  30624  ubthlem1  30800  ubthlem3  30802  minvecolem7  30813  chocunii  31231  pjhthmo  31232  pjhthlem2  31322  nmopub2tALT  31839  nmfnleub2  31856  kbass5  32050  mdslmd1lem1  32255  mdslmd1lem2  32256  mdsymlem5  32337  fcobij  32636  xrofsup  32674  mgcf1o  32876  xrge0tsmsd  32930  symgcntz  32967  archiabllem2a  33063  gsumvsca1  33094  gsumvsca2  33095  isarchiofld  33200  prmidl2  33322  ssmxidl  33355  constrelextdg2  33619  smatrcl  33624  reff  33667  ordtconnlem1  33752  qqhval2  33810  esumpcvgval  33924  imambfm  34109  ballotlemsf1o  34360  signstfvneq0  34431  pconnconn  35072  connpconn  35076  cvmliftmo  35125  cvmlift2lem10  35153  cvmlift2lem12  35155  cvmlift3lem7  35166  mrsubff1  35355  msubff1  35397  ifscgr  35881  cgrxfr  35892  btwnconn1lem13  35936  ellines  35989  unblimceq0lem  36222  unbdqndv2  36227  irrdiff  37046  matunitlindflem1  37330  poimirlem4  37338  poimirlem13  37347  poimirlem14  37348  heicant  37369  opnmbllem0  37370  mblfinlem3  37373  itg2addnclem  37385  itg2addnc  37388  ftc1cnnc  37406  sstotbnd  37489  cntotbnd  37510  ismtyima  37517  heibor1lem  37523  heiborlem10  37534  bfp  37538  rrncmslem  37546  islshpsm  38691  lsatcmp  38714  islshpat  38728  lfl0f  38780  iscvlat2N  39035  ishlat3N  39065  3dim1  39179  islvol5  39291  lvoli2  39293  lncvrelatN  39493  lncmp  39495  paddasslem10  39541  pclfinclN  39662  pexmidlem8N  39689  idltrn  39862  cdleme42keg  40198  cdleme42mgN  40200  cdlemf2  40274  cdlemg2cex  40303  trlcoat  40435  tendoex  40687  erngdvlem4  40703  erngdvlem4-rN  40711  dialss  40758  dibglbN  40878  diblss  40882  dihlsscpre  40946  dihglblem2aN  41005  dihglblem4  41009  dihglblem5  41010  dih1dimatlem  41041  dihglblem6  41052  lcfl7N  41213  lcfrlem9  41262  mapdh9a  41501  hdmapglem7  41641  aks4d1p8  41799  isprimroot  41805  evl1gprodd  41829  hashnexinjle  41841  deg1gprod  41852  sticksstones22  41880  grpods  41906  renegeulemv  42079  sn-subeu  42137  remulinvcom  42143  sn-itrere  42179  sn-retire  42180  imacrhmcl  42204  fidomncyc  42225  fsuppind  42280  prjspertr  42295  prjspreln0  42299  flt4lem7  42349  nna4b4nsq  42350  isnacs3  42404  nacsfix  42406  mzpsubst  42442  eldioph2lem2  42455  eldioph2  42456  eldioph2b  42457  diophin  42466  diophun  42467  rencldnfilem  42514  irrapxlem3  42518  irrapxlem5  42520  pell1234qrreccl  42548  pell1234qrmulcl  42549  pell1qrge1  42564  pell1qrgaplem  42567  monotuz  42636  monotoddzzfi  42637  acongtr  42673  acongrep  42675  jm2.26a  42695  jm2.26lem3  42696  jm2.26  42697  jm2.27b  42701  jm2.27  42703  wepwsolem  42740  fnwe2lem2  42749  hbtlem5  42826  hbt  42828  mpaaeu  42848  cantnftermord  43023  cantnfresb  43027  omabs2  43035  tfsconcatun  43040  tfsconcatfn  43041  tfsconcatfv1  43042  tfsconcatfv2  43043  tfsconcatfv  43044  tfsconcatrn  43045  naddcnff  43065  oaun3lem1  43077  rfovcnvf1od  43708  mnurndlem1  43992  fnchoice  44665  rfcnnnub  44672  disjxp1  44707  ioondisj2  45147  iccintsng  45177  fprodcn  45257  lptioo2  45288  lptioo1  45289  limclner  45308  dvdsn1add  45596  stoweidlem14  45671  stoweidlem27  45684  stoweidlem34  45691  stoweidlem49  45706  stoweidlem56  45713  fourierdlem87  45850  iundjiun  46117  ismeannd  46124  hoidmvle  46257  prproropf1olem2  47112  perfectALTVlem2  47330  mogoldbb  47393  bgoldbtbndlem2  47414  bgoldbtbndlem3  47415  rngcinvALTV  47689  ringcinvALTV  47723  mndpsuppss  47786  lindslinindsimp2lem5  47881  itscnhlinecirc02p  48209  toslat  48344  functhinclem4  48401
  Copyright terms: Public domain W3C validator