Theorem simpli 458

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpli.1

Assertion

Ref	Expression
simpli

Proof of Theorem simpli

Step	Hyp	Ref	Expression
1		simpli.1	. 2
2		simpl 457	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  /\wa 369

This theorem is referenced by:  pwundif  4792  tfr2b  7084  rdgfun  7101  oeoa  7265  oeoe  7267  ssdomg  7581  ordtypelem4  7967  ordtypelem6  7969  ordtypelem7  7970  r1limg  8210  rankwflemb  8232  r1elssi  8244  infxpenlem  8412  ackbij2  8644  wunom  9119  mulnzcnopr  10220  negiso  10544  infmsup  10546  hashunlei  12483  hashsslei  12484  cos01bnd  13921  cos1bnd  13922  cos2bnd  13923  sin4lt0  13930  egt2lt3  13939  epos  13940  divalglem5  14055  bitsf1o  14095  gcdaddmlem  14166  strlemor1  14724  zrhpsgnmhm  18620  resubgval  18645  re1r  18649  redvr  18653  refld  18655  txindis  20135  icopnfhmeo  21443  iccpnfcnv  21444  iccpnfhmeo  21445  xrhmeo  21446  cnheiborlem  21454  rrxcph  21824  volf  21940  i1f1  22097  itg11  22098  dvsin  22383  taylthlem2  22769  reefgim  22845  pilem3  22848  pigt2lt4  22849  pire  22851  pipos  22853  sinhalfpi  22861  tan4thpi  22907  sincos3rdpi  22909  circgrp  22939  circsubm  22940  rzgrp  22941  1cubrlem  23172  1cubr  23173  jensenlem2  23317  amgmlem  23319  emcllem6  23330  emcllem7  23331  emgt0  23336  harmonicbnd3  23337  ppiublem1  23477  chtub  23487  bposlem7  23565  lgsdir2lem4  23601  lgsdir2lem5  23602  chebbnd1  23657  mulog2sumlem2  23720  pntpbnd1a  23770  pntpbnd2  23772  pntlemb  23782  pntlemk  23791  qrng0  23806  qrng1  23807  qrngneg  23808  qrngdiv  23809  qabsabv  23814  2trllemE  24555  normlem7tALT  26036  hhsssh  26185  shintcli  26247  chintcli  26249  omlsi  26322  qlaxr3i  26554  lnophm  26938  nmcopex  26948  nmcoplb  26949  nmbdfnlbi  26968  nmcfnex  26972  nmcfnlb  26973  hmopidmch  27072  hmopidmpj  27073  chirred  27314  nn0archi  27833  xrge0iifiso  27917  xrge0iifmhm  27921  xrge0pluscn  27922  rezh  27952  qqh0  27965  qqh1  27966  qqhcn  27972  qqhucn  27973  rerrext  27990  cnrrext  27991  mbfmvolf  28237  subfacval3  28633  erdszelem5  28639  erdszelem8  28642  ghomgrpilem2  29026  filnetlem3  30198  filnetlem4  30199  reheibor  30335  fourierdlem68  31957  fourierdlem77  31966  fourierdlem80  31969  fouriersw  32014  etransclem23  32040  abcdta  32117  abcdtb  32118  abcdtc  32119  zlmodzxzsubm  32948  zlmodzxzldeplem3  33103  ldepsnlinclem1  33106  ldepsnlinclem2  33107  ldepsnlinc  33109  ene1  33168  empty-surprise  33197

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 185  df-an 371