Theorem simprbi 275

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 120	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simprd 114	1 |- ( ph -> ch )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.63dc  955  sb1  1815  reurmo  2766  eldifn  3346  elinel2  3410  rabsnt  3771  eldifsni  3827  unimax  3953  ssintub  3972  exmidsssnc  4321  moop2  4373  wepo  4485  wetrep  4486  trssord  4506  ordelord  4507  ordsucim  4627  ordtri2or2exmidlem  4653  regexmidlem1  4660  reg2exmidlema  4661  tfis  4710  opelxp2  4789  funmo  5372  funopg  5391  funco  5397  funun  5402  fununi  5429  funimaexglem  5444  fndm  5460  frn  5522  f1ss  5584  f1ssr  5585  f1ssres  5587  forn  5598  f1f1orn  5630  f1orescnv  5635  f1imacnv  5636  funcocnv2  5644  funfveu  5688  nfvres  5711  isorel  5987  isoini2  5998  f1ofveu  6046  fovcld  6166  f1opw  6270  f1o2ndf1  6437  mpoxopn0yelv  6483  swoer  6808  mapsnconst  6942  en0  7048  en1  7052  phplem4  7122  phplem4dom  7129  phplem4on  7135  ssfilem  7143  ssfilemd  7145  diffitest  7157  inffiexmid  7179  fsuppcorn  7267  supubti  7303  suplubti  7304  djuinr  7367  casefun  7389  casef1  7394  djufun  7408  nnnninfeq  7432  ctssexmid  7454  exmidonfinlem  7509  exmidfodomrlemim  7517  cc4f  7599  cc4n  7601  0npi  7644  mulclpi  7659  mulcanpig  7666  nlt1pig  7672  indpi  7673  nnppipi  7674  dfplpq2  7685  archnqq  7748  enq0tr  7765  nqnq0pi  7769  ltexprlemopl  7932  ltexprlemopu  7934  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemdisj  8033  suplocsrlempr  8138  ltresr2  8171  peano2nnnn  8184  axrnegex  8210  ltxrlt  8355  peano2nn  9266  elnn0z  9607  zaddcl  9634  ztri3or0  9636  eluz2gt1  9952  1nuz2  9956  rpgt0  10016  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccss2  10296  iccssico2  10299  elfzuz3  10375  uzdisj  10449  nn0disj  10494  zsupcllemstep  10611  zsupssdc  10622  addmodlteq  10784  expge0  10961  expge1  10962  expaddzaplem  10968  shftfn  11534  fsumf1o  12101  fsumge0  12170  fprodf1o  12299  bitsfzolem  12665  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  bezoutlemsup  12730  1nprm  12836  nprm  12845  sqnprm  12858  dvdsprm  12859  coprm  12866  sqpweven  12897  2sqpwodd  12898  dfphi2  12942  phimullem  12947  eulerthlemrprm  12951  phisum  12963  expnprm  13076  1arith  13090  4sqlem18  13131  ballotfilem4  13185  ballotfilem5  13186  ballotfilemfrc  13214  ballotfilemirc  13219  ballotfilemth  13225  oddennn  13227  znnen  13233  ennnfonelemg  13238  ctinf  13265  mndid  13686  mhmf  13720  mhmlin  13722  mhm0  13723  grpinvex  13765  grplinv  13805  mulgz  13903  mulgdirlem  13906  mulgdir  13907  mulgass  13912  nsgbi  13957  nmzbi  13962  ghmf  14000  ghmlin  14001  conjnsg  14034  ablcmn  14044  cmncom  14055  crngmgp  14247  rhmmhm  14404  rhmghm  14407  rimf1o  14415  nzrnz  14427  subrgss  14468  subrg1cl  14475  rrgeq0i  14510  domneq0  14519  fldcrngd  14554  2idlelbas  14790  2idlcpblrng  14797  znidomb  14932  toponuni  15006  tpsuni  15025  neipsm  15145  cnf  15195  cnima  15211  txdis1cn  15269  hmeocnvcn  15297  psmetxrge0  15323  isxmet2d  15339  xmstopn  15446  mstopn  15447  bdxmet  15492  divcnap  15556  ivthinclemlr  15628  ivthinclemur  15630  dvlemap  15671  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  dveflem  15717  plyf  15728  plyadd  15742  plymul  15743  plycn  15753  dvply2g  15757  dvdsppwf1o  15983  mpodvdsmulf1o  15984  lgsfle1  16008  lgsle1  16014  lgsdirprm  16033  lgsne0  16037  lgsquadlem1  16076  lgsquadlem2  16077  upgr1or2  16222  umgredg2en  16230  lfgredg2dom  16253  upgr2wlkdc  16498  trlres  16511  clwwlknon  16550  bj-indsuc  16824  nnsf  16909