Theorem simprbi 273

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simprbi.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
simprbi	|- ( ph -> ch )

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 119	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simprd 113	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.63dc  936  sb1  1754  reurmo  2680  eldifn  3245  elinel2  3309  rabsnt  3651  eldifsni  3705  unimax  3823  ssintub  3842  exmidsssnc  4182  moop2  4229  wepo  4337  wetrep  4338  trssord  4358  ordelord  4359  ordsucim  4477  ordtri2or2exmidlem  4503  regexmidlem1  4510  reg2exmidlema  4511  tfis  4560  opelxp2  4639  funmo  5203  funopg  5222  funco  5228  funun  5232  fununi  5256  funimaexglem  5271  fndm  5287  frn  5346  f1ss  5399  f1ssr  5400  f1ssres  5402  forn  5413  f1f1orn  5443  f1orescnv  5448  f1imacnv  5449  funcocnv2  5457  funfveu  5499  nfvres  5519  isorel  5776  isoini2  5787  f1ofveu  5830  fovcl  5947  f1opw  6045  f1o2ndf1  6196  mpoxopn0yelv  6207  swoer  6529  mapsnconst  6660  en0  6761  en1  6765  phplem4  6821  phplem4dom  6828  phplem4on  6833  ssfilem  6841  diffitest  6853  inffiexmid  6872  supubti  6964  suplubti  6965  djuinr  7028  casefun  7050  casef1  7055  djufun  7069  nnnninfeq  7092  ctssexmid  7114  exmidonfinlem  7149  exmidfodomrlemim  7157  cc4f  7210  cc4n  7212  0npi  7254  mulclpi  7269  mulcanpig  7276  nlt1pig  7282  indpi  7283  nnppipi  7284  dfplpq2  7295  archnqq  7358  enq0tr  7375  nqnq0pi  7379  ltexprlemopl  7542  ltexprlemopu  7544  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemupu  7590  cauappcvgprlemdisj  7592  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemupu  7613  caucvgprlemdisj  7615  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemupu  7641  caucvgprprlemdisj  7643  suplocsrlempr  7748  ltresr2  7781  peano2nnnn  7794  axrnegex  7820  ltxrlt  7964  peano2nn  8869  elnn0z  9204  zaddcl  9231  ztri3or0  9233  eluz2gt1  9540  1nuz2  9544  rpgt0  9601  ixxss1  9840  ixxss2  9841  ixxss12  9842  iccss2  9880  iccssico2  9883  elfzuz3  9957  uzdisj  10028  nn0disj  10073  addmodlteq  10333  expge0  10491  expge1  10492  expaddzaplem  10498  shftfn  10766  fsumf1o  11331  fsumge0  11400  fprodf1o  11529  zsupcllemstep  11878  zsupssdc  11887  bezoutlemzz  11935  bezoutlemaz  11936  bezoutlembz  11937  bezoutlemsup  11942  1nprm  12046  nprm  12055  sqnprm  12068  dvdsprm  12069  coprm  12076  sqpweven  12107  2sqpwodd  12108  dfphi2  12152  phimullem  12157  eulerthlemrprm  12161  phisum  12172  expnprm  12283  1arith  12297  oddennn  12325  znnen  12331  ennnfonelemg  12336  ctinf  12363  toponuni  12653  tpsuni  12672  neipsm  12794  cnf  12844  cnima  12860  txdis1cn  12918  hmeocnvcn  12946  psmetxrge0  12972  isxmet2d  12988  xmstopn  13095  mstopn  13096  bdxmet  13141  divcnap  13195  ivthinclemlr  13255  ivthinclemur  13257  dvlemap  13289  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  dvrecap  13317  dveflem  13327  lgsfle1  13550  lgsle1  13556  lgsdirprm  13575  lgsne0  13579  bj-indsuc  13810  nnsf  13885