Theorem simpl 443

Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Assertion

Ref	Expression
simpl	|- ((ph /\ ps) -> ph)

Proof of Theorem simpl

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 |- (ph -> (ps -> ph))
2	1	imp 418	1 |- ((ph /\ ps) -> ph)

Syntax hints:   -> wi 4   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  simpli  444  simpld  445  adantrd  454  iba  489  pm3.41  542  pm4.45im  545  prth  554  pm4.44  560  pm4.71  611  adantlr  695  adantrr  697  adantllr  699  adantlrr  701  adantrlr  703  adantrrr  705  simplll  734  simplrl  736  simprll  738  simprrl  740  anabs1  783  jcab  833  pm4.39  841  pm4.38  842  intnanr  881  intnanrd  883  dedlema  920  dedlemb  921  prlem2  929  simp1l  979  simp2l  981  simp3l  983  3anandis  1283  nic-ax  1438  nic-axALT  1439  exsimpl  1592  19.26  1593  sbequ2  1650  mooran1  2258  euan  2261  eupickbi  2270  2eu2  2285  dimatis  2320  r19.26  2747  r19.40  2763  rr19.28v  2982  eueq3  3012  reu6  3026  sbc2iegf  3113  sbcralt  3119  rmob  3135  csbiebt  3173  ssab2  3351  uneqin  3507  undif3  3516  ifan  3702  difsn  3846  unissel  3921  ssmin  3946  unissint  3951  uniintsn  3964  iota4an  4359  iota2  4368  reiota2  4369  peano1  4403  nnsucelr  4429  ltfintr  4460  ncfineleq  4478  eqtfinrelk  4487  sfinltfin  4536  ncvspfin  4539  vfinspsslem1  4551  phi11lem1  4596  mosubopt  4613  opabssxp  4838  ideqg2  4870  dmcoss  4972  xpcan2  5059  dfxp2  5114  fun11uni  5163  fnbr  5186  fvopab3ig  5388  ffnfv  5428  ffvresb  5432  isomin  5497  f1oiso  5500  fnoprabg  5586  ovmpt2x  5713  fvfullfunlem2  5863  erth  5969  erdisj  5973  ecelqsdm  5995  elnc  6126  pw1fin  6170  dflec3  6222  nchoicelem6  6295  nchoicelem8  6297