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

Theorem simplrl 796
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 759 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 196  df-an 385
This theorem is referenced by:  disjxiun  4579  disjxiunOLD  4580  f1imass  6422  f1prex  6439  soisoi  6478  riota5f  6535  tfrlem9a  7369  oeeui  7569  oaabs2  7612  omabs  7614  omxpenlem  7946  fopwdom  7953  frfi  8090  marypha1lem  8222  ordiso2  8303  oismo  8328  wemaplem3  8336  cantnf  8473  isinffi  8701  dfac12lem2  8849  dfac12lem3  8850  infxp  8920  infmap2  8923  infpssrlem5  9012  fin23lem11  9022  fin23lem24  9027  fin23lem26  9030  isf32lem2  9059  isf32lem4  9061  fin1a2lem13  9117  fin1a2s  9119  ttukeylem5  9218  fpwwe2lem12  9342  fpwwe2lem13  9343  wunex2  9439  tskord  9481  prlem934  9734  mulcmpblnr  9771  dedekind  10079  addid1  10095  cnegex  10096  negeu  10150  add20  10419  divdivdiv  10605  ltmul12a  10758  lediv12a  10795  cru  10889  uzwo3  11659  xleadd1a  11955  xlemul1a  11990  ixxun  12062  ixxss12  12066  elfz0ubfz0  12312  mulexpz  12762  leexp1a  12781  expmulnbnd  12858  swrdccat3  13343  abs3lem  13926  rexanre  13934  cau3lem  13942  lo1bdd2  14103  o1lo1  14116  rlimclim1  14124  rlimclim  14125  lo1resb  14143  o1resb  14145  rlimcn2  14169  o1of2  14191  o1rlimmul  14197  lo1add  14205  lo1mul  14206  isercolllem1  14243  climcau  14249  summolem2  14294  summo  14295  o1fsum  14386  prodmolem2  14504  qredeu  15210  isprm5  15257  pclem  15381  pcqmul  15396  pcexp  15402  pcneg  15416  pcprmpw2  15424  pcadd  15431  prmpwdvds  15446  4sqlem13  15499  vdwlem2  15524  vdwlem7  15529  vdwlem11  15533  vdwlem12  15534  ramval  15550  ramz2  15566  ramcl  15571  prmgaplem6  15598  cshwshashlem2  15641  imasval  15994  imasdsval  15998  mreexexd  16131  mreexexdOLD  16132  issubc3  16332  idfucl  16364  funcres2c  16384  fucpropd  16460  xpcval  16640  prfval  16662  evlfcl  16685  curf12  16690  curf1cl  16691  curf2  16692  curfcl  16695  curfuncf  16701  curf2ndf  16710  hof2val  16719  hofcl  16722  hofpropd  16730  yonedalem4a  16738  yonedainv  16744  poslubmo  16969  posglbmo  16970  isipodrs  16984  acsmapd  17001  acsinfd  17003  ismndd  17136  mndpropd  17139  mhmeql  17187  mrcmndind  17189  frmdup3lem  17226  mhmmnd  17360  issubg4  17436  ssnmz  17459  f1otrspeq  17690  psgneu  17749  sylow2blem3  17860  lsmdisj2  17918  pj1eu  17932  efgredlem  17983  frgpuplem  18008  frgpnabl  18101  dmdprdsplitlem  18259  pgpfac1lem3  18299  pgpfaclem3  18305  ringpropd  18405  dvdsrtr  18475  islmhm2  18859  lmhmpropd  18894  assapropd  19148  evlslem1  19336  coe1tmmul2  19467  prmirredlem  19660  psgndiflemA  19766  lsmcss  19855  dsmmlss  19907  uvcf1  19950  frlmup1  19956  mamucl  20026  mamuass  20027  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  mamulid  20066  mamurid  20067  dmatsubcl  20123  dmatmulcl  20125  mdetunilem7  20243  mdetunilem9  20245  cramer0  20315  cpmatmcllem  20342  mat2pmatf1  20353  decpmatmul  20396  pmatcollpw1  20400  pm2mpf1lem  20418  pm2mpmhmlem2  20443  chpidmat  20471  cpmadugsumlemB  20498  cpmadugsumlemC  20499  toponmre  20707  restbas  20772  iscncl  20883  cnpdis  20907  lmcnp  20918  dishaus  20996  cmpcovf  21004  hauscmplem  21019  dfcon2  21032  clscon  21043  2ndcctbss  21068  1stccnp  21075  islly2  21097  llyidm  21101  cldllycmp  21108  locfincmp  21139  kgentopon  21151  1stckgenlem  21166  ptpjpre1  21184  ptbasfi  21194  txcls  21217  ptpjopn  21225  xkoccn  21232  txcnp  21233  txcmpb  21257  xkoptsub  21267  xkoco2cn  21271  xkoinjcn  21300  qtopcn  21327  qtoprest  21330  regr1lem  21352  regr1lem2  21353  kqreglem1  21354  qtophmeo  21430  fgabs  21493  hauspwpwf1  21601  flimfnfcls  21642  fclscmp  21644  cnpfcf  21655  ptcmplem4  21669  ptcmplem5  21670  cnextfval  21676  cnextfun  21678  tmdgsum2  21710  tsmsval2  21743  utoptop  21848  utop3cls  21865  ismet2  21948  blin  22036  metss2lem  22126  methaus  22135  met1stc  22136  met2ndci  22137  metcnp  22156  metcnpi3  22161  metustto  22168  metustfbas  22172  nlmvscn  22301  nrginvrcn  22306  nghmcn  22359  xrsxmet  22420  reconnlem1  22437  reconn  22439  xrge0tsms  22445  xmetdcn2  22448  metdscn  22467  addcnlem  22475  mulc1cncf  22516  cncfco  22518  cnheiborlem  22561  cnheibor  22562  nmoleub2lem2  22724  ipcn  22853  iscfil3  22879  cfilfcls  22880  iscmet3  22899  caubl  22914  bcthlem5  22933  rrxdstprj1  23000  minveclem3b  23007  minveclem7  23014  pmltpc  23026  ovolshftlem1  23084  ovolscalem1  23088  ioombl1  23137  uniioombllem6  23162  dyadss  23168  dyaddisjlem  23169  dyadmax  23172  opnmbllem  23175  itg1addlem2  23270  itg2seq  23315  bddmulibl  23411  limcfval  23442  ellimc3  23449  limciun  23464  dveflem  23546  rolle  23557  dvlip2  23562  c1liplem1  23563  dvgt0lem1  23569  dvgt0  23571  dvlt0  23572  dvne0  23578  dvcnvre  23586  dvfsumrlimge0  23597  ftc1lem6  23608  itgsubst  23616  mdegmullem  23642  ply1domn  23687  fta1g  23731  fta1b  23733  dgrlem  23789  coeid  23798  plydivalg  23858  aannenlem1  23887  aalioulem6  23896  ulmcn  23957  mtestbdd  23963  abelthlem8  23997  efif1olem4  24095  chordthm  24364  xrlimcnp  24495  lgamgulmlem5  24559  isppw2  24641  fsumvma2  24739  perfectlem2  24755  lgsdilem  24849  lgsquad2lem2  24910  lgsquad3  24912  2sqlem5  24947  2sqlem9  24952  rpvmasumlem  24976  dchrisum0flb  24999  pntpbnd  25077  pntibndlem3  25081  pntlem3  25098  pntleml  25100  tgbtwnconn1lem3  25269  legtrid  25286  tglinethru  25331  tglnpt2  25336  tglineintmo  25337  mirreu3  25349  perpcom  25408  footex  25413  mideu  25430  opphllem1  25439  lnopp2hpgb  25455  axsegcon  25607  axpasch  25621  axeuclidlem  25642  ecgrtg  25663  elntg  25664  eengtrkg  25665  upgr1eopALT  25783  usgrasscusgra  26011  4cycl4dv4e  26196  wwlknext  26252  clwwisshclwwlem  26334  usg2spthonot1  26417  eupath2  26507  usg2spot2nb  26592  numclwlk1lem2foa  26618  numclwwlk6  26640  vacn  26933  ubthlem1  27110  ubthlem3  27112  minvecolem7  27123  chocunii  27544  pjhthmo  27545  pjhthlem2  27635  nmopub2tALT  28152  nmfnleub2  28169  kbass5  28363  mdslmd1lem1  28568  mdslmd1lem2  28569  mdsymlem5  28650  fcobij  28888  xrofsup  28923  archiabllem2a  29079  gsumvsca1  29113  gsumvsca2  29114  xrge0tsmsd  29116  isarchiofld  29148  smatrcl  29190  reff  29234  ordtconlem1  29298  qqhval2  29354  esumpcvgval  29467  imambfm  29651  ballotlemsf1o  29902  signstfvneq0  29975  pconcon  30467  conpcon  30471  cvmliftmo  30520  cvmlift2lem10  30548  cvmlift2lem12  30550  cvmlift3lem7  30561  mrsubff1  30665  msubff1  30707  ifscgr  31321  cgrxfr  31332  btwnconn1lem13  31376  ellines  31429  unblimceq0lem  31667  unbdqndv2  31672  matunitlindflem1  32575  poimirlem4  32583  poimirlem13  32592  poimirlem14  32593  heicant  32614  opnmbllem0  32615  mblfinlem3  32618  itg2addnclem  32631  itg2addnc  32634  ftc1cnnc  32654  sstotbnd  32744  cntotbnd  32765  ismtyima  32772  heibor1lem  32778  heiborlem10  32789  bfp  32793  rrncmslem  32801  islshpsm  33285  lsatcmp  33308  islshpat  33322  lfl0f  33374  iscvlat2N  33629  ishlat3N  33659  3dim1  33771  islvol5  33883  lvoli2  33885  lncvrelatN  34085  lncmp  34087  paddasslem10  34133  pclfinclN  34254  pexmidlem8N  34281  idltrn  34454  cdleme42keg  34792  cdleme42mgN  34794  cdlemf2  34868  cdlemg2cex  34897  trlcoat  35029  tendoex  35281  erngdvlem4  35297  erngdvlem4-rN  35305  dialss  35353  dibglbN  35473  diblss  35477  dihlsscpre  35541  dihglblem2aN  35600  dihglblem4  35604  dihglblem5  35605  dih1dimatlem  35636  dihglblem6  35647  lcfl7N  35808  lcfrlem9  35857  mapdh9a  36097  hdmapglem7  36239  isnacs3  36291  nacsfix  36293  mzpsubst  36329  eldioph2lem2  36342  eldioph2  36343  eldioph2b  36344  diophin  36354  diophun  36355  rencldnfilem  36402  irrapxlem3  36406  irrapxlem5  36408  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell1qrge1  36452  pell1qrgaplem  36455  monotuz  36524  monotoddzzfi  36525  rpexpmord  36531  acongtr  36563  acongrep  36565  jm2.26a  36585  jm2.26lem3  36586  jm2.26  36587  jm2.27b  36591  jm2.27  36593  wepwsolem  36630  fnwe2lem2  36639  hbtlem5  36717  hbt  36719  mpaaeu  36739  rfovcnvf1od  37318  fnchoice  38211  rfcnnnub  38218  disjxp1  38263  ioondisj2  38561  iccintsng  38596  fprodcn  38667  lptioo2  38698  lptioo1  38699  limclner  38718  dvdsn1add  38829  stoweidlem14  38907  stoweidlem27  38920  stoweidlem34  38927  stoweidlem49  38942  stoweidlem56  38949  fourierdlem87  39086  iundjiun  39353  ismeannd  39360  hoidmvle  39490  perfectALTVlem2  40165  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  pfxccat3  40289  usgredg4  40444  usgr1eop  40476  usgr1v  40482  subuhgr  40510  subumgr  40512  subusgr  40513  nbuhgr2vtx1edgb  40574  wwlksnext  41099  usgr2wspthon  41168  clwwisshclwwslem  41234  n4cyclfrgr  41461  frgr2wwlkeu  41492  av-numclwlk1lem2foa  41521  mgmhmeql  41593  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  mndpsuppss  41946  lindslinindsimp2lem5  42045
  Copyright terms: Public domain W3C validator