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  2211  opabss  4093  euotd  4283  wetriext  4609  sosng  4732  xpsspw  4771  brcogw  4831  funimaexglem  5337  funfni  5354  fnco  5362  fnssres  5367  fn0  5373  fnimadisj  5374  fnimaeq0  5375  foco  5487  foimacnv  5518  fvelimab  5613  fvopab3ig  5631  dff3im  5703  dffo4  5706  fmptco  5724  f1eqcocnv  5834  f1ocnv2d  6122  fnexALT  6163  xp1st  6218  xp2nd  6219  tfrlemiubacc  6383  tfri2d  6389  tfr1onlemubacc  6399  tfrcllemubacc  6412  tfri3  6420  ecelqsg  6642  elqsn0m  6657  fidifsnen  6926  recclnq  7452  nq0a0  7517  qreccl  9707  difelfzle  10200  exfzdc  10307  modifeq2int  10457  frec2uzlt2d  10475  zzlesq  10779  1elfz0hash  10877  lennncl  10934  wrdsymb0  10946  caucvgrelemcau  11124  recvalap  11241  fzomaxdiflem  11256  2zsupmax  11369  2zinfmin  11386  fsumparts  11613  ntrivcvgap  11691  divconjdvds  11991  ndvdssub  12071  zsupcllemstep  12082  rplpwr  12164  dvdssqlem  12167  eucalgcvga  12196  mulgcddvds  12232  isprm2lem  12254  powm2modprm  12390  coprimeprodsq  12395  pythagtriplem11  12412  pythagtriplem13  12414  pcadd2  12479  4sqlem11  12539  grpidd  12966  ismndd  13018  gsumfzz  13067  gsumwmhm  13070  mulgaddcom  13216  resghm  13330  conjnsg  13351  isrngd  13449  isringd  13537  01eq0ring  13685  lspsneq0b  13923  lmodindp1  13924  znf1o  14139  uniopn  14169  ntrval  14278  clsval  14279  neival  14311  restdis  14352  lmbrf  14383  cnpnei  14387  dviaddf  14854  dvimulf  14855  logbgt0b  15098  lgslem4  15119  lgsmod  15142  lgsdir2lem2  15145  lgsdir2  15149  lgsne0  15154  lgsmulsqcoprm  15162  lgseisenlem1  15186  2sqlem4  15205