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  8452  rdgfun  8472  oeoa  8653  oeoe  8655  ssdomg  9060  ordtypelem4  9590  ordtypelem6  9592  ordtypelem7  9593  r1limg  9840  rankwflemb  9862  r1elssi  9874  infxpenlem  10082  ackbij2  10311  wunom  10789  mulnzcnf  11936  negiso  12275  infrenegsup  12278  hashunlei  14474  hashsslei  14475  cos01bnd  16234  cos1bnd  16235  cos2bnd  16236  sin4lt0  16243  egt2lt3  16254  epos  16255  ene1  16258  divalglem5  16445  bitsf1o  16491  gcdaddmlem  16570  sravsca  21208  zrhpsgnmhm  21625  resubgval  21650  re1r  21654  redvr  21658  refld  21660  rzgrp  21664  txindis  23663  icopnfhmeo  24993  iccpnfcnv  24994  iccpnfhmeo  24995  xrhmeo  24996  cnheiborlem  25005  recvs  25198  recvsOLD  25199  qcvs  25200  rrxcph  25445  volf  25583  i1f1  25744  itg11  25745  dvsin  26040  taylthlem2  26434  taylthlem2OLD  26435  reefgim  26512  pilem3  26515  pigt2lt4  26516  pire  26518  pipos  26520  sinhalfpi  26528  tan4thpi  26574  tan4thpiOLD  26575  sincos3rdpi  26577  pigt3  26578  circgrp  26612  circsubm  26613  1cubrlem  26902  1cubr  26903  jensenlem2  27049  amgmlem  27051  emcllem6  27062  emcllem7  27063  harmonicbnd3  27069  ppiublem1  27264  chtub  27274  bposlem7  27352  lgsdir2lem4  27390  lgsdir2lem5  27391  chebbnd1  27534  mulog2sumlem2  27597  pntpbnd1a  27647  pntpbnd2  27649  pntlemb  27659  pntlemk  27668  qrng0  27683  qrng1  27684  qrngneg  27685  qrngdiv  27686  qabsabv  27691  ex-sqrt  30486  normlem7tALT  31151  hhsssh  31301  shintcli  31361  chintcli  31363  omlsi  31436  qlaxr3i  31668  lnophm  32051  nmcopex  32061  nmcoplb  32062  nmbdfnlbi  32081  nmcfnex  32085  nmcfnlb  32086  hmopidmch  32185  hmopidmpj  32186  chirred  32427  threehalves  32879  1fldgenq  33289  nn0archi  33340  ccfldextrr  33661  ccfldsrarelvec  33681  2sqr3minply  33738  xrge0iifiso  33881  xrge0iifmhm  33885  xrge0pluscn  33886  rezh  33917  qqh0  33930  qqh1  33931  qqhcn  33937  qqhucn  33938  rerrext  33955  cnrrext  33956  mbfmvolf  34231  hgt750lem  34628  subfacval3  35157  erdszelem5  35163  erdszelem8  35166  filnetlem3  36346  filnetlem4  36347  bj-genr  36572  bj-genl  36573  bj-genan  36574  bj-rveccmod  37268  reheibor  37799  cossssid  38423  eqvrelcoss3  38574  3lexlogpow5ineq5  42017  aks6d1c7lem1  42137  tan3rdpi  42338  asin1half  42339  fourierdlem68  46095  fourierdlem77  46104  fourierdlem80  46107  fouriersw  46152  etransclem23  46178  gsumge0cl  46292  abcdta  46840  abcdtb  46841  abcdtc  46842  nabctnabc  46846  zlmodzxzsubm  48084  zlmodzxzldeplem3  48231  ldepsnlinclem1  48234  ldepsnlinclem2  48235  ldepsnlinc  48237  sepfsepc  48607  prstcleval  48735  prstcocval  48738  empty-surprise  48876  amgmwlem  48896  amgmlemALT  48897