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 486 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 726 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  disjxiun  5027  f1imass  7000  f1prex  7018  soisoi  7060  riota5f  7121  tfrlem9a  8005  oeeui  8211  oaabs2  8255  omabs  8257  omxpenlem  8601  fopwdom  8608  frfi  8747  marypha1lem  8881  ordiso2  8963  oismo  8988  wemaplem3  8996  cantnf  9140  isinffi  9405  dfac12lem2  9555  dfac12lem3  9556  infxp  9626  infmap2  9629  infpssrlem5  9718  fin23lem11  9728  fin23lem24  9733  fin23lem26  9736  isf32lem2  9765  isf32lem4  9767  fin1a2lem13  9823  fin1a2s  9825  ttukeylem5  9924  fpwwe2lem12  10052  fpwwe2lem13  10053  wunex2  10149  tskord  10191  prlem934  10444  mulcmpblnr  10482  dedekind  10792  addid1  10809  cnegex  10810  negeu  10865  add20  11141  divdivdiv  11330  ltmul12a  11485  lediv12a  11522  cru  11617  uzwo3  12331  xleadd1a  12634  xlemul1a  12669  ixxun  12742  ixxss12  12746  elfz0ubfz0  13006  mulexpz  13465  rpexpmord  13528  leexp1a  13535  expmulnbnd  13592  swrdccatin1  14078  pfxccatin12lem3  14085  pfxccat3  14087  abs3lem  14690  rexanre  14698  cau3lem  14706  lo1bdd2  14873  o1lo1  14886  rlimclim1  14894  rlimclim  14895  lo1resb  14913  o1resb  14915  rlimcn2  14939  o1of2  14961  o1rlimmul  14967  lo1add  14975  lo1mul  14976  isercolllem1  15013  climcau  15019  summolem2  15065  summo  15066  o1fsum  15160  prodmolem2  15281  qredeu  15992  isprm5  16041  pclem  16165  pcqmul  16180  pcexp  16186  pcneg  16200  pcprmpw2  16208  pcadd  16215  prmpwdvds  16230  4sqlem13  16283  vdwlem2  16308  vdwlem7  16313  vdwlem11  16317  vdwlem12  16318  ramval  16334  ramz2  16350  ramcl  16355  prmgaplem6  16382  cshwshashlem2  16422  imasval  16776  imasdsval  16780  mreexexd  16911  issubc3  17111  idfucl  17143  funcres2c  17163  fucpropd  17239  xpcval  17419  prfval  17441  evlfcl  17464  curf12  17469  curf1cl  17470  curf2  17471  curfcl  17474  curfuncf  17480  curf2ndf  17489  hof2val  17498  hofcl  17501  hofpropd  17509  yonedalem4a  17517  yonedainv  17523  poslubmo  17748  posglbmo  17749  isipodrs  17763  acsmapd  17780  acsinfd  17782  ismndd  17925  mndpropd  17928  mhmeql  17982  mndind  17984  frmdup3lem  18023  mhmmnd  18213  issubg4  18290  ssnmz  18310  f1otrspeq  18567  psgneu  18626  sylow2blem3  18739  lsmdisj2  18800  pj1eu  18814  efgredlem  18865  frgpuplem  18890  frgpnabl  18988  dmdprdsplitlem  19152  pgpfac1lem3  19192  pgpfaclem3  19198  ablsimpgcygd  19221  ringpropd  19328  dvdsrtr  19398  islmhm2  19803  lmhmpropd  19838  prmirredlem  20186  psgndiflemA  20290  lsmcss  20381  dsmmlss  20433  uvcf1  20481  frlmup1  20487  assapropd  20558  evlslem1  20754  coe1tmmul2  20905  mamucl  21006  mamuass  21007  mamudi  21008  mamudir  21009  mamuvs1  21010  mamuvs2  21011  mamulid  21046  mamurid  21047  dmatsubcl  21103  dmatmulcl  21105  mdetunilem7  21223  mdetunilem9  21225  cramer0  21295  cpmatmcllem  21323  mat2pmatf1  21334  decpmatmul  21377  pmatcollpw1  21381  pm2mpf1lem  21399  pm2mpmhmlem2  21424  chpidmat  21452  cpmadugsumlemB  21479  cpmadugsumlemC  21480  toponmre  21698  restbas  21763  iscncl  21874  cnpdis  21898  lmcnp  21909  dishaus  21987  cmpcovf  21996  hauscmplem  22011  dfconn2  22024  clsconn  22035  2ndcctbss  22060  1stccnp  22067  islly2  22089  llyidm  22093  cldllycmp  22100  locfincmp  22131  kgentopon  22143  1stckgenlem  22158  ptpjpre1  22176  ptbasfi  22186  txcls  22209  ptpjopn  22217  xkoccn  22224  txcnp  22225  txcmpb  22249  xkoptsub  22259  xkoco2cn  22263  xkoinjcn  22292  qtopcn  22319  qtoprest  22322  regr1lem  22344  regr1lem2  22345  kqreglem1  22346  qtophmeo  22422  fgabs  22484  hauspwpwf1  22592  flimfnfcls  22633  fclscmp  22635  cnpfcf  22646  ptcmplem4  22660  ptcmplem5  22661  cnextfval  22667  cnextfun  22669  tmdgsum2  22701  tsmsval2  22735  utoptop  22840  utop3cls  22857  ismet2  22940  blin  23028  metss2lem  23118  methaus  23127  met1stc  23128  met2ndci  23129  metcnp  23148  metcnpi3  23153  metustto  23160  metustfbas  23164  nlmvscn  23293  nrginvrcn  23298  nghmcn  23351  xrsxmet  23414  reconnlem1  23431  reconn  23433  xrge0tsms  23439  xmetdcn2  23442  metdscn  23461  addcnlem  23469  mulc1cncf  23510  cncfco  23512  cnheiborlem  23559  cnheibor  23560  nmoleub2lem2  23721  ipcn  23850  iscfil3  23877  cfilfcls  23878  iscmet3  23897  caubl  23912  bcthlem5  23932  rrxdstprj1  24013  minveclem3b  24032  minveclem7  24039  pmltpc  24054  ovolshftlem1  24113  ovolscalem1  24117  ioombl1  24166  uniioombllem6  24192  dyadss  24198  dyaddisjlem  24199  dyadmax  24202  opnmbllem  24205  itg1addlem2  24301  itg2seq  24346  bddmulibl  24442  limcfval  24475  ellimc3  24482  limciun  24497  dveflem  24582  rolle  24593  dvlip2  24598  c1liplem1  24599  dvgt0lem1  24605  dvgt0  24607  dvlt0  24608  dvne0  24614  dvcnvre  24622  dvfsumrlimge0  24633  ftc1lem6  24644  itgsubst  24652  mdegmullem  24679  ply1domn  24724  fta1g  24768  fta1b  24770  dgrlem  24826  coeid  24835  plydivalg  24895  aannenlem1  24924  aalioulem6  24933  ulmcn  24994  mtestbdd  25000  abelthlem8  25034  efif1olem4  25137  chordthm  25423  xrlimcnp  25554  lgamgulmlem5  25618  isppw2  25700  fsumvma2  25798  perfectlem2  25814  lgsdilem  25908  lgsquad2lem2  25969  lgsquad3  25971  2sqlem5  26006  2sqlem9  26011  rpvmasumlem  26071  dchrisum0flb  26094  pntpbnd  26172  pntibndlem3  26176  pntlem3  26193  pntleml  26195  tgjustc1  26269  tgjustc2  26270  tgbtwnconn1lem3  26368  legtrid  26385  tglinethru  26430  tglnpt2  26435  tglineintmo  26436  mirreu3  26448  perpcom  26507  footexALT  26512  footex  26515  mideu  26532  opphllem1  26541  lnopp2hpgb  26557  axsegcon  26721  axpasch  26735  axeuclidlem  26756  ecgrtg  26777  elntg  26778  eengtrkg  26780  upgr1eopALT  26910  usgredg4  27007  usgr1eop  27040  usgr1v  27046  subuhgr  27076  subumgr  27078  subusgr  27079  nbuhgr2vtx1edgb  27142  wwlksnext  27679  usgr2wspthon  27751  clwlkclwwlkf1  27795  clwwisshclwwslem  27799  n4cyclfrgr  28076  dlwwlknondlwlknonf1o  28150  vacn  28477  ubthlem1  28653  ubthlem3  28655  minvecolem7  28666  chocunii  29084  pjhthmo  29085  pjhthlem2  29175  nmopub2tALT  29692  nmfnleub2  29709  kbass5  29903  mdslmd1lem1  30108  mdslmd1lem2  30109  mdsymlem5  30190  fcobij  30484  xrofsup  30518  xrge0tsmsd  30742  symgcntz  30779  archiabllem2a  30873  gsumvsca1  30904  gsumvsca2  30905  isarchiofld  30941  prmidl2  31024  ssmxidl  31050  smatrcl  31149  reff  31192  ordtconnlem1  31277  qqhval2  31333  esumpcvgval  31447  imambfm  31630  ballotlemsf1o  31881  signstfvneq0  31952  pconnconn  32591  connpconn  32595  cvmliftmo  32644  cvmlift2lem10  32672  cvmlift2lem12  32674  cvmlift3lem7  32685  mrsubff1  32874  msubff1  32916  frpomin  33191  noprefixmo  33315  noetalem3  33332  slerec  33390  ifscgr  33618  cgrxfr  33629  btwnconn1lem13  33673  ellines  33726  unblimceq0lem  33958  unbdqndv2  33963  irrdiff  34740  matunitlindflem1  35053  poimirlem4  35061  poimirlem13  35070  poimirlem14  35071  heicant  35092  opnmbllem0  35093  mblfinlem3  35096  itg2addnclem  35108  itg2addnc  35111  ftc1cnnc  35129  sstotbnd  35213  cntotbnd  35234  ismtyima  35241  heibor1lem  35247  heiborlem10  35258  bfp  35262  rrncmslem  35270  islshpsm  36276  lsatcmp  36299  islshpat  36313  lfl0f  36365  iscvlat2N  36620  ishlat3N  36650  3dim1  36763  islvol5  36875  lvoli2  36877  lncvrelatN  37077  lncmp  37079  paddasslem10  37125  pclfinclN  37246  pexmidlem8N  37273  idltrn  37446  cdleme42keg  37782  cdleme42mgN  37784  cdlemf2  37858  cdlemg2cex  37887  trlcoat  38019  tendoex  38271  erngdvlem4  38287  erngdvlem4-rN  38295  dialss  38342  dibglbN  38462  diblss  38466  dihlsscpre  38530  dihglblem2aN  38589  dihglblem4  38593  dihglblem5  38594  dih1dimatlem  38625  dihglblem6  38636  lcfl7N  38797  lcfrlem9  38846  mapdh9a  39085  hdmapglem7  39225  fsuppind  39454  renegeulemv  39504  sn-subeu  39561  remulinvcom  39567  itrere  39589  retire  39590  prjspertr  39597  prjspreln0  39601  isnacs3  39649  nacsfix  39651  mzpsubst  39687  eldioph2lem2  39700  eldioph2  39701  eldioph2b  39702  diophin  39711  diophun  39712  rencldnfilem  39759  irrapxlem3  39763  irrapxlem5  39765  pell1234qrreccl  39793  pell1234qrmulcl  39794  pell1qrge1  39809  pell1qrgaplem  39812  monotuz  39880  monotoddzzfi  39881  acongtr  39917  acongrep  39919  jm2.26a  39939  jm2.26lem3  39940  jm2.26  39941  jm2.27b  39945  jm2.27  39947  wepwsolem  39984  fnwe2lem2  39993  hbtlem5  40070  hbt  40072  mpaaeu  40092  rfovcnvf1od  40703  mnurndlem1  40987  fnchoice  41656  rfcnnnub  41663  disjxp1  41701  ioondisj2  42128  iccintsng  42158  fprodcn  42240  lptioo2  42271  lptioo1  42272  limclner  42291  dvdsn1add  42579  stoweidlem14  42654  stoweidlem27  42667  stoweidlem34  42674  stoweidlem49  42689  stoweidlem56  42696  fourierdlem87  42833  iundjiun  43097  ismeannd  43104  hoidmvle  43237  prproropf1olem2  44019  perfectALTVlem2  44238  mogoldbb  44301  bgoldbtbndlem2  44322  bgoldbtbndlem3  44323  mgmhmeql  44421  rngcinv  44603  rngcinvALTV  44615  ringcinv  44654  ringcinvALTV  44678  mndpsuppss  44771  lindslinindsimp2lem5  44869  itscnhlinecirc02p  45197
  Copyright terms: Public domain W3C validator