Theorem biimpar 295

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimpar	|- ( ( ph /\ ch ) -> ps )

Proof of Theorem biimpar

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimprd 157	. 2 |- ( ph -> ( ch -> ps ) )
3	2	imp 123	1 |- ( ( ph /\ ch ) -> ps )

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  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exbiri  380  bitr  469  eqtr  2188  opabss  4053  euotd  4239  wetriext  4561  sosng  4684  xpsspw  4723  brcogw  4780  funimaexglem  5281  funfni  5298  fnco  5306  fnssres  5311  fn0  5317  fnimadisj  5318  fnimaeq0  5319  foco  5430  foimacnv  5460  fvelimab  5552  fvopab3ig  5570  dff3im  5641  dffo4  5644  fmptco  5662  f1eqcocnv  5770  f1ocnv2d  6053  fnexALT  6090  xp1st  6144  xp2nd  6145  tfrlemiubacc  6309  tfri2d  6315  tfr1onlemubacc  6325  tfrcllemubacc  6338  tfri3  6346  ecelqsg  6566  elqsn0m  6581  fidifsnen  6848  recclnq  7354  nq0a0  7419  qreccl  9601  difelfzle  10090  exfzdc  10196  modifeq2int  10342  frec2uzlt2d  10360  1elfz0hash  10741  caucvgrelemcau  10944  recvalap  11061  fzomaxdiflem  11076  2zsupmax  11189  2zinfmin  11206  fsumparts  11433  ntrivcvgap  11511  divconjdvds  11809  ndvdssub  11889  zsupcllemstep  11900  rplpwr  11982  dvdssqlem  11985  eucalgcvga  12012  mulgcddvds  12048  isprm2lem  12070  powm2modprm  12206  coprimeprodsq  12211  pythagtriplem11  12228  pythagtriplem13  12230  grpidd  12637  ismndd  12673  uniopn  12793  ntrval  12904  clsval  12905  neival  12937  restdis  12978  lmbrf  13009  cnpnei  13013  dviaddf  13463  dvimulf  13464  logbgt0b  13678  lgslem4  13698  lgsmod  13721  lgsdir2lem2  13724  lgsdir2  13728  lgsne0  13733  lgsmulsqcoprm  13741  2sqlem4  13748