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  2746  r19.40  2762  rr19.28v  2981  eueq3  3011  reu6  3025  sbc2iegf  3112  sbcralt  3118  rmob  3134  csbiebt  3172  ssab2  3350  uneqin  3506  undif3  3515  ifan  3701  difsn  3845  unissel  3920  ssmin  3945  unissint  3950  uniintsn  3963  iota4an  4358  iota2  4367  reiota2  4368  peano1  4402  nnsucelr  4428  ltfintr  4459  ncfineleq  4477  eqtfinrelk  4486  sfinltfin  4535  ncvspfin  4538  vfinspsslem1  4550  phi11lem1  4595  mosubopt  4612  opabssxp  4837  ideqg2  4869  dmcoss  4971  xpcan2  5058  dfxp2  5113  fun11uni  5162  fnbr  5185  fvopab3ig  5387  ffnfv  5427  ffvresb  5431  isomin  5496  f1oiso  5499  fnoprabg  5585  ovmpt2x  5712  fvfullfunlem2  5862  erth  5968  erdisj  5972  ecelqsdm  5994  elnc  6125  pw1fin  6169  dflec3  6221  nchoicelem6  6294  nchoicelem8  6296