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  8325  rdgfun  8345  oeoa  8522  oeoe  8524  ssdomg  8932  ordtypelem4  9432  ordtypelem6  9434  ordtypelem7  9435  r1limg  9686  rankwflemb  9708  r1elssi  9720  infxpenlem  9926  ackbij2  10155  wunom  10633  mulnzcnf  11784  negiso  12123  infrenegsup  12126  hashunlei  14350  hashsslei  14351  cos01bnd  16113  cos1bnd  16114  cos2bnd  16115  sin4lt0  16122  egt2lt3  16133  epos  16134  ene1  16137  divalglem5  16326  bitsf1o  16374  gcdaddmlem  16453  sravsca  21103  zrhpsgnmhm  21509  resubgval  21534  re1r  21538  redvr  21542  refld  21544  rzgrp  21548  txindis  23537  icopnfhmeo  24857  iccpnfcnv  24858  iccpnfhmeo  24859  xrhmeo  24860  cnheiborlem  24869  recvs  25062  qcvs  25063  rrxcph  25308  volf  25446  i1f1  25607  itg11  25608  dvsin  25902  taylthlem2  26298  taylthlem2OLD  26299  reefgim  26376  pilem3  26379  pigt2lt4  26380  pire  26382  pipos  26384  sinhalfpi  26393  tan4thpi  26439  tan4thpiOLD  26440  sincos3rdpi  26442  pigt3  26443  circgrp  26477  circsubm  26478  1cubrlem  26767  1cubr  26768  jensenlem2  26914  amgmlem  26916  emcllem6  26927  emcllem7  26928  harmonicbnd3  26934  ppiublem1  27129  chtub  27139  bposlem7  27217  lgsdir2lem4  27255  lgsdir2lem5  27256  chebbnd1  27399  mulog2sumlem2  27462  pntpbnd1a  27512  pntpbnd2  27514  pntlemb  27524  pntlemk  27533  qrng0  27548  qrng1  27549  qrngneg  27550  qrngdiv  27551  qabsabv  27556  ex-sqrt  30416  normlem7tALT  31081  hhsssh  31231  shintcli  31291  chintcli  31293  omlsi  31366  qlaxr3i  31598  lnophm  31981  nmcopex  31991  nmcoplb  31992  nmbdfnlbi  32011  nmcfnex  32015  nmcfnlb  32016  hmopidmch  32115  hmopidmpj  32116  chirred  32357  threehalves  32868  qfld  33246  1fldgenq  33271  nn0archi  33294  ccfldextrr  33618  ccfldsrarelvec  33642  constrextdg2  33715  constrext2chnlem  33716  constrcon  33740  2sqr3minply  33746  2sqr3nconstr  33747  cos9thpiminplylem6  33753  cos9thpiminply  33754  cos9thpinconstrlem2  33756  trisecnconstr  33758  xrge0iifiso  33901  xrge0iifmhm  33905  xrge0pluscn  33906  rezh  33935  qqh0  33950  qqh1  33951  qqhcn  33957  qqhucn  33958  rerrext  33975  cnrrext  33976  mbfmvolf  34233  hgt750lem  34618  subfacval3  35161  erdszelem5  35167  erdszelem8  35170  filnetlem3  36353  filnetlem4  36354  bj-genr  36579  bj-genl  36580  bj-genan  36581  bj-rveccmod  37275  reheibor  37818  cossssid  38443  eqvrelcoss3  38594  3lexlogpow5ineq5  42033  aks6d1c7lem1  42153  tan3rdpi  42325  sin2t3rdpi  42326  sin4t3rdpi  42328  asin1half  42330  fourierdlem68  46156  fourierdlem77  46165  fourierdlem80  46168  fouriersw  46213  etransclem23  46239  gsumge0cl  46353  abcdta  46910  abcdtb  46911  abcdtc  46912  nabctnabc  46916  zlmodzxzsubm  48344  zlmodzxzldeplem3  48488  ldepsnlinclem1  48491  ldepsnlinclem2  48492  ldepsnlinc  48494  sepfsepc  48913  prstcleval  49541  prstcocval  49543  setc1onsubc  49588  empty-surprise  49768  amgmwlem  49788  amgmlemALT  49789