Theorem simpli 483

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

Syntax hints:   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  tfr2b  8410  rdgfun  8430  oeoa  8609  oeoe  8611  ssdomg  9014  ordtypelem4  9535  ordtypelem6  9537  ordtypelem7  9538  r1limg  9785  rankwflemb  9807  r1elssi  9819  infxpenlem  10027  ackbij2  10256  wunom  10734  mulnzcnf  11883  negiso  12222  infrenegsup  12225  hashunlei  14443  hashsslei  14444  cos01bnd  16204  cos1bnd  16205  cos2bnd  16206  sin4lt0  16213  egt2lt3  16224  epos  16225  ene1  16228  divalglem5  16416  bitsf1o  16464  gcdaddmlem  16543  sravsca  21139  zrhpsgnmhm  21544  resubgval  21569  re1r  21573  redvr  21577  refld  21579  rzgrp  21583  txindis  23572  icopnfhmeo  24892  iccpnfcnv  24893  iccpnfhmeo  24894  xrhmeo  24895  cnheiborlem  24904  recvs  25097  recvsOLD  25098  qcvs  25099  rrxcph  25344  volf  25482  i1f1  25643  itg11  25644  dvsin  25938  taylthlem2  26334  taylthlem2OLD  26335  reefgim  26412  pilem3  26415  pigt2lt4  26416  pire  26418  pipos  26420  sinhalfpi  26429  tan4thpi  26475  tan4thpiOLD  26476  sincos3rdpi  26478  pigt3  26479  circgrp  26513  circsubm  26514  1cubrlem  26803  1cubr  26804  jensenlem2  26950  amgmlem  26952  emcllem6  26963  emcllem7  26964  harmonicbnd3  26970  ppiublem1  27165  chtub  27175  bposlem7  27253  lgsdir2lem4  27291  lgsdir2lem5  27292  chebbnd1  27435  mulog2sumlem2  27498  pntpbnd1a  27548  pntpbnd2  27550  pntlemb  27560  pntlemk  27569  qrng0  27584  qrng1  27585  qrngneg  27586  qrngdiv  27587  qabsabv  27592  ex-sqrt  30435  normlem7tALT  31100  hhsssh  31250  shintcli  31310  chintcli  31312  omlsi  31385  qlaxr3i  31617  lnophm  32000  nmcopex  32010  nmcoplb  32011  nmbdfnlbi  32030  nmcfnex  32034  nmcfnlb  32035  hmopidmch  32134  hmopidmpj  32135  chirred  32376  threehalves  32889  qfld  33291  1fldgenq  33316  nn0archi  33362  ccfldextrr  33688  ccfldsrarelvec  33712  constrextdg2  33783  constrext2chnlem  33784  constrcon  33808  2sqr3minply  33814  2sqr3nconstr  33815  cos9thpiminplylem6  33821  cos9thpiminply  33822  xrge0iifiso  33966  xrge0iifmhm  33970  xrge0pluscn  33971  rezh  34000  qqh0  34015  qqh1  34016  qqhcn  34022  qqhucn  34023  rerrext  34040  cnrrext  34041  mbfmvolf  34298  hgt750lem  34683  subfacval3  35211  erdszelem5  35217  erdszelem8  35220  filnetlem3  36398  filnetlem4  36399  bj-genr  36624  bj-genl  36625  bj-genan  36626  bj-rveccmod  37320  reheibor  37863  cossssid  38485  eqvrelcoss3  38636  3lexlogpow5ineq5  42073  aks6d1c7lem1  42193  tan3rdpi  42399  asin1half  42400  fourierdlem68  46203  fourierdlem77  46212  fourierdlem80  46215  fouriersw  46260  etransclem23  46286  gsumge0cl  46400  abcdta  46954  abcdtb  46955  abcdtc  46956  nabctnabc  46960  zlmodzxzsubm  48334  zlmodzxzldeplem3  48478  ldepsnlinclem1  48481  ldepsnlinclem2  48482  ldepsnlinc  48484  sepfsepc  48902  prstcleval  49432  prstcocval  49434  setc1onsubc  49479  empty-surprise  49646  amgmwlem  49666  amgmlemALT  49667