Theorem simplbi 274

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

Hypothesis

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

Assertion

Ref	Expression
simplbi	|- ( ph -> ps )

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 120	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simpld 112	1 |- ( ph -> ps )

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an3  591  pm5.62dc  953  3simpa  1020  xoror  1423  anxordi  1444  sbidm  1899  reurex  2752  eqimss  3281  eldifi  3329  elinel1  3393  inss1  3427  sopo  4410  wefr  4455  ordtr  4475  opelxp1  4759  relop  4880  ssrelrn  4922  funmo  5341  funrel  5343  funinsn  5379  fnfun  5427  ffn  5482  f1f  5542  f1of1  5582  f1ofo  5590  isof1o  5948  eqopi  6335  1st2nd2  6338  reldmtpos  6419  swoer  6730  ecopover  6802  ecopoverg  6805  fnfi  7135  casef  7287  nninff  7321  lpowlpo  7367  dfplpq2  7574  enq0ref  7653  cauappcvgprlemopl  7866  cauappcvgprlemdisj  7871  caucvgprlemopl  7889  caucvgprlemdisj  7894  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemdisj  7922  peano1nnnn  8072  axrnegex  8099  ltxrlt  8245  1nn  9154  zre  9483  nnssz  9496  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  rge0ssre  10212  elfzuz  10256  uzdisj  10328  nn0disj  10373  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  0wrd0  11143  modfsummodlemstep  12036  mertenslem2  12115  prmnn  12700  prmuz2  12721  oddpwdc  12764  sqpweven  12765  2sqpwodd  12766  phimullem  12815  hashgcdlem  12828  1arith  12958  ctinfom  13067  ctinf  13069  sgrpmgm  13508  mndsgrp  13522  grpmnd  13608  nsgsubg  13810  ghmgrp1  13850  ghmgrp2  13851  ablgrp  13894  cmnmnd  13906  crngring  14040  rimrhm  14204  subrgring  14257  subrgrcl  14259  rhmpropd  14287  domnnzr  14303  2idlelbas  14549  rng2idlsubgsubrng  14553  2idlcpblrng  14556  2idlcpbl  14557  qusrhm  14561  psr1clfi  14721  topontop  14757  tpstop  14778  cntop1  14944  cntop2  14945  hmeocn  15048  isxmet2d  15091  metxmet  15098  xmstps  15200  msxms  15201  xmsxmet  15203  msmet  15204  bdxmet  15244  ivthinclemlr  15380  ivthinclemur  15382  mpodvdsmulf1o  15733  uhgr0vb  15954  trliswlk  16256  eupthfi  16321  eupthistrl  16324  bj-indint  16577  bj-inf2vnlem2  16617  peano4nninf  16659