Theorem pm3.26i 320

Description: Inference eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.26i.1	⊢ (φ ⋀ ψ)

Assertion

Ref	Expression
pm3.26i	⊢ φ

Proof of Theorem pm3.26i

Step	Hyp	Ref	Expression
1		pm3.26i.1	. 2 ⊢ (φ ⋀ ψ)
2		pm3.26 319	. 2 ⊢ ((φ ⋀ ψ) → φ)
3	1, 2	ax-mp 7	1 ⊢ φ

Syntax hints:   ⋀ wa 223

This theorem is referenced by:  ssid 2070  ersym 4256  ssdomg 4389  xpmapenlem3 4478  xpmapenlem5 4480  ssrankr1 4648  pre-axlttri 5259  pre-axlttrn 5260  mulnzcnopr 5671  div11t 5721  recrect 5732  climunii 7035  caucvg3t 7104  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  isumsplit 7151  expcnvlem2 7163  expcnvlem4 7165  geolim 7172  geolim1 7174  negfcncf 7204  ivthlem4 7219  ivthlem5 7220  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  ivthlem9 7224  isupivth 7225  dsupivthlem 7226  ivthlem4OLD 7228  ivthlem5OLD 7229  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  ivthOLD 7233  ivth2OLD 7234  efseq1ex 7248  erelem4 7264  ele3lem 7268  ege2le3lem2 7271  absef01tlub 7329  eirrlem2 7331  eflegeolem2 7354  efcnlem4 7362  reeff1olem2 7365  reeff1olem2OLD 7367  reeff1o 7368  cos01bndlem3 7413  cos1bnd 7416  cos2bnd 7417  sin4lt0 7423  infunabs 7508  infcdaabs 7509  unctb 7519  bcth 7966  ghgrpilem1 8070  ghgrpilem2 8071  ghgrpilem3 8072  ghgrpilem4 8073  sinco 8586  cosco 8587  pilem1 8590  pilem2 8591  pilem3 8592  sinhalfpi 8599  efifolem1 8637  h2hsm 8783  normlem7tALT 8906  hlimunii 9029  hhsssh 9059  projlem7 9108  omls 9161  shintcl 9208  chintcl 9210  qlaxr3 9494  lnophmt 9859  nmcopext 9874  nmcoplbt 9875  nmbdfnlb 9893  nmcfnext 9903  nmcfnlbt 9904  hmopidmchlem 9989  hmopidmch 9990  hmopidmpj 9991  irredt 10230  ghomgrpilem2 10291

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain