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  618  eqtr  2250  opabss  4174  euotd  4371  wetriext  4699  sosng  4823  xpsspw  4862  brcogw  4924  funimaexglem  5439  funfni  5458  fnco  5466  fnssres  5471  fn0  5478  fnimadisj  5479  fnimaeq0  5480  foco  5601  foimacnv  5632  fvelimab  5733  fvopab3ig  5751  dff3im  5822  dffo4  5825  fmptco  5843  f1eqcocnv  5964  f1ocnv2d  6259  fnexALT  6304  xp1st  6359  xp2nd  6360  tfrlemiubacc  6561  tfri2d  6567  tfr1onlemubacc  6577  tfrcllemubacc  6590  tfri3  6598  ecelqsg  6822  elqsn0m  6837  fidifsnen  7125  pr1or2  7491  recclnq  7707  nq0a0  7772  qreccl  9974  difelfzle  10468  exfzdc  10586  zsupcllemstep  10589  modifeq2int  10748  frec2uzlt2d  10766  zzlesq  11070  fihashgt0  11170  1elfz0hash  11171  lennncl  11244  wrdsymb0  11257  ccatsymb  11290  ccatlid  11294  ccatass  11296  ccatswrd  11362  swrdccat2  11363  ccatpfx  11393  swrdccatfn  11416  swrdccat  11427  caucvgrelemcau  11665  recvalap  11782  fzomaxdiflem  11797  2zsupmax  11911  2zinfmin  11928  fsumparts  12156  ntrivcvgap  12234  fsumdvds  12528  divconjdvds  12535  ndvdssub  12616  rplpwr  12723  dvdssqlem  12726  eucalgcvga  12755  mulgcddvds  12791  isprm2lem  12813  powm2modprm  12950  coprimeprodsq  12955  pythagtriplem11  12972  pythagtriplem13  12974  pcadd2  13039  4sqlem11  13099  grpidd  13596  ismndd  13650  gsumfzz  13708  gsumwmhm  13711  mulgaddcom  13863  resghm  13977  conjnsg  13998  isrngd  14097  isringd  14185  01eq0ring  14334  lspsneq0b  14575  lmodindp1  14576  znf1o  14799  psrgrp  14840  uniopn  14866  ntrval  14975  clsval  14976  neival  15008  restdis  15049  lmbrf  15080  cnpnei  15084  dviaddf  15570  dvimulf  15571  logbgt0b  15831  pellexlem2  15846  perfectlem2  15868  lgslem4  15876  lgsmod  15899  lgsdir2lem2  15902  lgsdir2  15906  lgsne0  15911  lgsmulsqcoprm  15919  lgseisenlem1  15943  2lgsoddprm  15986  2sqlem4  15991  wlk1walkdom  16354  wlkreslem  16373