Theorem biimpar 297

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 158	. 2 |- ( ph -> ( ch -> ps ) )
3	2	imp 124	1 |- ( ( ph /\ ch ) -> 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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exbiri  382  bitr  472  biadanid  614  eqtr  2214  opabss  4097  euotd  4287  wetriext  4613  sosng  4736  xpsspw  4775  brcogw  4835  funimaexglem  5341  funfni  5358  fnco  5366  fnssres  5371  fn0  5377  fnimadisj  5378  fnimaeq0  5379  foco  5491  foimacnv  5522  fvelimab  5617  fvopab3ig  5635  dff3im  5707  dffo4  5710  fmptco  5728  f1eqcocnv  5838  f1ocnv2d  6127  fnexALT  6168  xp1st  6223  xp2nd  6224  tfrlemiubacc  6388  tfri2d  6394  tfr1onlemubacc  6404  tfrcllemubacc  6417  tfri3  6425  ecelqsg  6647  elqsn0m  6662  fidifsnen  6931  recclnq  7459  nq0a0  7524  qreccl  9716  difelfzle  10209  exfzdc  10316  zsupcllemstep  10319  modifeq2int  10478  frec2uzlt2d  10496  zzlesq  10800  1elfz0hash  10898  lennncl  10955  wrdsymb0  10967  caucvgrelemcau  11145  recvalap  11262  fzomaxdiflem  11277  2zsupmax  11391  2zinfmin  11408  fsumparts  11635  ntrivcvgap  11713  fsumdvds  12007  divconjdvds  12014  ndvdssub  12095  rplpwr  12194  dvdssqlem  12197  eucalgcvga  12226  mulgcddvds  12262  isprm2lem  12284  powm2modprm  12421  coprimeprodsq  12426  pythagtriplem11  12443  pythagtriplem13  12445  pcadd2  12510  4sqlem11  12570  grpidd  13026  ismndd  13078  gsumfzz  13127  gsumwmhm  13130  mulgaddcom  13276  resghm  13390  conjnsg  13411  isrngd  13509  isringd  13597  01eq0ring  13745  lspsneq0b  13983  lmodindp1  13984  znf1o  14207  uniopn  14237  ntrval  14346  clsval  14347  neival  14379  restdis  14420  lmbrf  14451  cnpnei  14455  dviaddf  14941  dvimulf  14942  logbgt0b  15202  perfectlem2  15236  lgslem4  15244  lgsmod  15267  lgsdir2lem2  15270  lgsdir2  15274  lgsne0  15279  lgsmulsqcoprm  15287  lgseisenlem1  15311  2lgsoddprm  15354  2sqlem4  15359