Theorem simpli 484

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 483	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ∧ wa 396

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 397

This theorem is referenced by:  pwundifOLD  5487  tfr2b  8236  rdgfun  8256  oeoa  8437  oeoe  8439  ssdomg  8795  ordtypelem4  9289  ordtypelem6  9291  ordtypelem7  9292  r1limg  9538  rankwflemb  9560  r1elssi  9572  infxpenlem  9778  ackbij2  10008  wunom  10485  mulnzcnopr  11630  negiso  11964  infrenegsup  11967  hashunlei  14149  hashsslei  14150  cos01bnd  15904  cos1bnd  15905  cos2bnd  15906  sin4lt0  15913  egt2lt3  15924  epos  15925  ene1  15928  divalglem5  16115  bitsf1o  16161  gcdaddmlem  16240  sravsca  20458  zrhpsgnmhm  20798  resubgval  20823  re1r  20827  redvr  20831  refld  20833  rzgrp  20837  txindis  22794  icopnfhmeo  24115  iccpnfcnv  24116  iccpnfhmeo  24117  xrhmeo  24118  cnheiborlem  24126  recvs  24318  recvsOLD  24319  qcvs  24320  rrxcph  24565  volf  24702  i1f1  24863  itg11  24864  dvsin  25155  taylthlem2  25542  reefgim  25618  pilem3  25621  pigt2lt4  25622  pire  25624  pipos  25626  sinhalfpi  25634  tan4thpi  25680  sincos3rdpi  25682  pigt3  25683  circgrp  25717  circsubm  25718  1cubrlem  26000  1cubr  26001  jensenlem2  26146  amgmlem  26148  emcllem6  26159  emcllem7  26160  harmonicbnd3  26166  ppiublem1  26359  chtub  26369  bposlem7  26447  lgsdir2lem4  26485  lgsdir2lem5  26486  chebbnd1  26629  mulog2sumlem2  26692  pntpbnd1a  26742  pntpbnd2  26744  pntlemb  26754  pntlemk  26763  qrng0  26778  qrng1  26779  qrngneg  26780  qrngdiv  26781  qabsabv  26786  ex-sqrt  28827  normlem7tALT  29490  hhsssh  29640  shintcli  29700  chintcli  29702  omlsi  29775  qlaxr3i  30007  lnophm  30390  nmcopex  30400  nmcoplb  30401  nmbdfnlbi  30420  nmcfnex  30424  nmcfnlb  30425  hmopidmch  30524  hmopidmpj  30525  chirred  30766  threehalves  31198  nn0archi  31556  ccfldextrr  31732  ccfldsrarelvec  31750  xrge0iifiso  31894  xrge0iifmhm  31898  xrge0pluscn  31899  rezh  31930  qqh0  31943  qqh1  31944  qqhcn  31950  qqhucn  31951  rerrext  31968  cnrrext  31969  mbfmvolf  32242  hgt750lem  32640  subfacval3  33160  erdszelem5  33166  erdszelem8  33169  filnetlem3  34578  filnetlem4  34579  bj-genr  34797  bj-genl  34798  bj-genan  34799  bj-rveccmod  35482  reheibor  36006  cossssid  36592  eqvrelcoss3  36738  3lexlogpow5ineq5  40075  fourierdlem68  43722  fourierdlem77  43731  fourierdlem80  43734  fouriersw  43779  etransclem23  43805  gsumge0cl  43916  abcdta  44431  abcdtb  44432  abcdtc  44433  nabctnabc  44437  zlmodzxzsubm  45706  zlmodzxzldeplem3  45854  ldepsnlinclem1  45857  ldepsnlinclem2  45858  ldepsnlinc  45860  sepfsepc  46232  prstcleval  46360  prstcocval  46363  empty-surprise  46497  amgmwlem  46517  amgmlemALT  46518