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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 471 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 758 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  disjxiun  4573  disjxiunOLD  4574  f1imass  6399  f1prex  6416  soisoi  6455  riota5f  6512  tfrlem9a  7346  oeeui  7546  oaabs2  7589  omabs  7591  omxpenlem  7923  fopwdom  7930  frfi  8067  marypha1lem  8199  ordiso2  8280  oismo  8305  wemaplem3  8313  cantnf  8450  isinffi  8678  dfac12lem2  8826  dfac12lem3  8827  infxp  8897  infmap2  8900  infpssrlem5  8989  fin23lem11  8999  fin23lem24  9004  fin23lem26  9007  isf32lem2  9036  isf32lem4  9038  fin1a2lem13  9094  fin1a2s  9096  ttukeylem5  9195  fpwwe2lem12  9319  fpwwe2lem13  9320  wunex2  9416  tskord  9458  prlem934  9711  mulcmpblnr  9748  dedekind  10051  addid1  10067  cnegex  10068  negeu  10122  add20  10391  divdivdiv  10577  ltmul12a  10730  lediv12a  10767  cru  10861  uzwo3  11617  xleadd1a  11914  xlemul1a  11949  ixxun  12020  ixxss12  12024  elfz0ubfz0  12269  mulexpz  12719  leexp1a  12738  expmulnbnd  12815  swrdccat3  13291  abs3lem  13874  rexanre  13882  cau3lem  13890  lo1bdd2  14051  o1lo1  14064  rlimclim1  14072  rlimclim  14073  lo1resb  14091  o1resb  14093  rlimcn2  14117  o1of2  14139  o1rlimmul  14145  lo1add  14153  lo1mul  14154  isercolllem1  14191  climcau  14197  summolem2  14242  summo  14243  o1fsum  14334  prodmolem2  14452  qredeu  15158  isprm5  15205  pclem  15329  pcqmul  15344  pcexp  15350  pcneg  15364  pcprmpw2  15372  pcadd  15379  prmpwdvds  15394  4sqlem13  15447  vdwlem2  15472  vdwlem7  15477  vdwlem11  15481  vdwlem12  15482  ramval  15498  ramz2  15514  ramcl  15519  prmgaplem6  15546  cshwshashlem2  15589  imasval  15942  imasdsval  15946  mreexexd  16079  mreexexdOLD  16080  issubc3  16280  idfucl  16312  funcres2c  16332  fucpropd  16408  xpcval  16588  prfval  16610  evlfcl  16633  curf12  16638  curf1cl  16639  curf2  16640  curfcl  16643  curfuncf  16649  curf2ndf  16658  hof2val  16667  hofcl  16670  hofpropd  16678  yonedalem4a  16686  yonedainv  16692  poslubmo  16917  posglbmo  16918  isipodrs  16932  acsmapd  16949  acsinfd  16951  ismndd  17084  mndpropd  17087  mhmeql  17135  mrcmndind  17137  frmdup3lem  17174  mhmmnd  17308  issubg4  17384  ssnmz  17407  f1otrspeq  17638  psgneu  17697  sylow2blem3  17808  lsmdisj2  17866  pj1eu  17880  efgredlem  17931  frgpuplem  17956  frgpnabl  18049  dmdprdsplitlem  18207  pgpfac1lem3  18247  pgpfaclem3  18253  ringpropd  18353  dvdsrtr  18423  islmhm2  18807  lmhmpropd  18842  assapropd  19096  evlslem1  19284  coe1tmmul2  19415  prmirredlem  19607  psgndiflemA  19713  lsmcss  19802  dsmmlss  19854  uvcf1  19897  frlmup1  19903  mamucl  19973  mamuass  19974  mamudi  19975  mamudir  19976  mamuvs1  19977  mamuvs2  19978  mamulid  20013  mamurid  20014  dmatsubcl  20070  dmatmulcl  20072  mdetunilem7  20190  mdetunilem9  20192  cramer0  20262  cpmatmcllem  20289  mat2pmatf1  20300  decpmatmul  20343  pmatcollpw1  20347  pm2mpf1lem  20365  pm2mpmhmlem2  20390  chpidmat  20418  cpmadugsumlemB  20445  cpmadugsumlemC  20446  toponmre  20654  restbas  20719  iscncl  20830  cnpdis  20854  lmcnp  20865  dishaus  20943  cmpcovf  20951  hauscmplem  20966  dfcon2  20979  clscon  20990  2ndcctbss  21015  1stccnp  21022  islly2  21044  llyidm  21048  cldllycmp  21055  locfincmp  21086  kgentopon  21098  1stckgenlem  21113  ptpjpre1  21131  ptbasfi  21141  txcls  21164  ptpjopn  21172  xkoccn  21179  txcnp  21180  txcmpb  21204  xkoptsub  21214  xkoco2cn  21218  xkoinjcn  21247  qtopcn  21274  qtoprest  21277  regr1lem  21299  regr1lem2  21300  kqreglem1  21301  qtophmeo  21377  fgabs  21440  hauspwpwf1  21548  flimfnfcls  21589  fclscmp  21591  cnpfcf  21602  ptcmplem4  21616  ptcmplem5  21617  cnextfval  21623  cnextfun  21625  tmdgsum2  21657  tsmsval2  21690  utoptop  21795  utop3cls  21812  ismet2  21895  blin  21983  metss2lem  22073  methaus  22082  met1stc  22083  met2ndci  22084  metcnp  22103  metcnpi3  22108  metustto  22115  metustfbas  22119  nlmvscn  22248  nrginvrcn  22253  nghmcn  22306  xrsxmet  22367  reconnlem1  22384  reconn  22386  xrge0tsms  22392  xmetdcn2  22395  metdscn  22414  addcnlem  22422  mulc1cncf  22463  cncfco  22465  cnheiborlem  22508  cnheibor  22509  nmoleub2lem2  22671  ipcn  22797  iscfil3  22823  cfilfcls  22824  iscmet3  22843  caubl  22858  bcthlem5  22877  rrxdstprj1  22944  minveclem3b  22951  minveclem7  22958  pmltpc  22970  ovolshftlem1  23028  ovolscalem1  23032  ioombl1  23081  uniioombllem6  23106  dyadss  23112  dyaddisjlem  23113  dyadmax  23116  opnmbllem  23119  itg1addlem2  23214  itg2seq  23259  bddmulibl  23355  limcfval  23386  ellimc3  23393  limciun  23408  dveflem  23490  rolle  23501  dvlip2  23506  c1liplem1  23507  dvgt0lem1  23513  dvgt0  23515  dvlt0  23516  dvne0  23522  dvcnvre  23530  dvfsumrlimge0  23541  ftc1lem6  23552  itgsubst  23560  mdegmullem  23586  ply1domn  23631  fta1g  23675  fta1b  23677  dgrlem  23733  coeid  23742  plydivalg  23802  aannenlem1  23831  aalioulem6  23840  ulmcn  23901  mtestbdd  23907  abelthlem8  23941  efif1olem4  24039  chordthm  24308  xrlimcnp  24439  lgamgulmlem5  24503  isppw2  24585  fsumvma2  24683  perfectlem2  24699  lgsdilem  24793  lgsquad2lem2  24854  lgsquad3  24856  2sqlem5  24891  2sqlem9  24896  rpvmasumlem  24920  dchrisum0flb  24943  pntpbnd  25021  pntibndlem3  25025  pntlem3  25042  pntleml  25044  tgbtwnconn1lem3  25214  legtrid  25231  tglinethru  25276  tglnpt2  25281  tglineintmo  25282  mirreu3  25294  perpcom  25353  footex  25358  mideu  25375  opphllem1  25384  lnopp2hpgb  25400  axsegcon  25552  axpasch  25566  axeuclidlem  25587  ecgrtg  25608  elntg  25609  eengtrkg  25610  usgrasscusgra  25804  4cycl4dv4e  25989  wwlknext  26045  clwwisshclwwlem  26127  usg2spthonot1  26210  eupath2  26300  usg2spot2nb  26385  numclwlk1lem2foa  26411  numclwwlk6  26433  vacn  26726  ubthlem1  26903  ubthlem3  26905  minvecolem7  26916  chocunii  27337  pjhthmo  27338  pjhthlem2  27428  nmopub2tALT  27945  nmfnleub2  27962  kbass5  28156  mdslmd1lem1  28361  mdslmd1lem2  28362  mdsymlem5  28443  fcobij  28681  xrofsup  28716  archiabllem2a  28872  gsumvsca1  28906  gsumvsca2  28907  xrge0tsmsd  28909  isarchiofld  28941  smatrcl  28983  reff  29027  ordtconlem1  29091  qqhval2  29147  esumpcvgval  29260  imambfm  29444  ballotlemsf1o  29695  signstfvneq0  29768  pconcon  30260  conpcon  30264  cvmliftmo  30313  cvmlift2lem10  30341  cvmlift2lem12  30343  cvmlift3lem7  30354  mrsubff1  30458  msubff1  30500  ifscgr  31114  cgrxfr  31125  btwnconn1lem13  31169  ellines  31222  unblimceq0lem  31460  unbdqndv2  31465  matunitlindflem1  32358  poimirlem4  32366  poimirlem13  32375  poimirlem14  32376  heicant  32397  opnmbllem0  32398  mblfinlem3  32401  itg2addnclem  32414  itg2addnc  32417  ftc1cnnc  32437  sstotbnd  32527  cntotbnd  32548  ismtyima  32555  heibor1lem  32561  heiborlem10  32572  bfp  32576  rrncmslem  32584  islshpsm  33068  lsatcmp  33091  islshpat  33105  lfl0f  33157  iscvlat2N  33412  ishlat3N  33442  3dim1  33554  islvol5  33666  lvoli2  33668  lncvrelatN  33868  lncmp  33870  paddasslem10  33916  pclfinclN  34037  pexmidlem8N  34064  idltrn  34237  cdleme42keg  34575  cdleme42mgN  34577  cdlemf2  34651  cdlemg2cex  34680  trlcoat  34812  tendoex  35064  erngdvlem4  35080  erngdvlem4-rN  35088  dialss  35136  dibglbN  35256  diblss  35260  dihlsscpre  35324  dihglblem2aN  35383  dihglblem4  35387  dihglblem5  35388  dih1dimatlem  35419  dihglblem6  35430  lcfl7N  35591  lcfrlem9  35640  mapdh9a  35880  hdmapglem7  36022  isnacs3  36074  nacsfix  36076  mzpsubst  36112  eldioph2lem2  36125  eldioph2  36126  eldioph2b  36127  diophin  36137  diophun  36138  rencldnfilem  36185  irrapxlem3  36189  irrapxlem5  36191  pell1234qrreccl  36219  pell1234qrmulcl  36220  pell1qrge1  36235  pell1qrgaplem  36238  monotuz  36307  monotoddzzfi  36308  rpexpmord  36314  acongtr  36346  acongrep  36348  jm2.26a  36368  jm2.26lem3  36369  jm2.26  36370  jm2.27b  36374  jm2.27  36376  wepwsolem  36413  fnwe2lem2  36422  hbtlem5  36500  hbt  36502  mpaaeu  36522  rfovcnvf1od  37101  fnchoice  37994  rfcnnnub  38001  disjxp1  38046  ioondisj2  38344  iccintsng  38379  fprodcn  38450  lptioo2  38481  lptioo1  38482  limclner  38501  dvdsn1add  38612  stoweidlem14  38690  stoweidlem27  38703  stoweidlem34  38710  stoweidlem49  38725  stoweidlem56  38732  fourierdlem87  38869  iundjiun  39136  ismeannd  39143  hoidmvle  39273  perfectALTVlem2  39949  bgoldbtbndlem2  40006  bgoldbtbndlem3  40007  pfxccat3  40073  upgr1eopALT  40323  usgredg4  40425  usgr1eop  40457  usgr1v  40463  subuhgr  40491  subumgr  40493  subusgr  40494  nbuhgr2vtx1edgb  40555  wwlksnext  41080  usgr2wspthon  41149  clwwisshclwwslem  41215  n4cyclfrgr  41442  frgr2wwlkeu  41473  av-numclwlk1lem2foa  41502  mgmhmeql  41574  rngcinv  41754  rngcinvALTV  41766  ringcinv  41805  ringcinvALTV  41829  mndpsuppss  41927  lindslinindsimp2lem5  42026
  Copyright terms: Public domain W3C validator