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  616  eqtr  2247  opabss  4148  euotd  4341  wetriext  4669  sosng  4792  xpsspw  4831  brcogw  4891  funimaexglem  5404  funfni  5423  fnco  5431  fnssres  5436  fn0  5443  fnimadisj  5444  fnimaeq0  5445  foco  5559  foimacnv  5590  fvelimab  5690  fvopab3ig  5708  dff3im  5780  dffo4  5783  fmptco  5801  f1eqcocnv  5915  f1ocnv2d  6210  fnexALT  6256  xp1st  6311  xp2nd  6312  tfrlemiubacc  6476  tfri2d  6482  tfr1onlemubacc  6492  tfrcllemubacc  6505  tfri3  6513  ecelqsg  6735  elqsn0m  6750  fidifsnen  7032  pr1or2  7367  recclnq  7579  nq0a0  7644  qreccl  9837  difelfzle  10330  exfzdc  10446  zsupcllemstep  10449  modifeq2int  10608  frec2uzlt2d  10626  zzlesq  10930  1elfz0hash  11028  lennncl  11091  wrdsymb0  11104  ccatsymb  11137  ccatlid  11141  ccatass  11143  ccatswrd  11202  swrdccat2  11203  ccatpfx  11233  swrdccatfn  11256  swrdccat  11267  caucvgrelemcau  11491  recvalap  11608  fzomaxdiflem  11623  2zsupmax  11737  2zinfmin  11754  fsumparts  11981  ntrivcvgap  12059  fsumdvds  12353  divconjdvds  12360  ndvdssub  12441  rplpwr  12548  dvdssqlem  12551  eucalgcvga  12580  mulgcddvds  12616  isprm2lem  12638  powm2modprm  12775  coprimeprodsq  12780  pythagtriplem11  12797  pythagtriplem13  12799  pcadd2  12864  4sqlem11  12924  grpidd  13416  ismndd  13470  gsumfzz  13528  gsumwmhm  13531  mulgaddcom  13683  resghm  13797  conjnsg  13818  isrngd  13916  isringd  14004  01eq0ring  14153  lspsneq0b  14391  lmodindp1  14392  znf1o  14615  psrgrp  14649  uniopn  14675  ntrval  14784  clsval  14785  neival  14817  restdis  14858  lmbrf  14889  cnpnei  14893  dviaddf  15379  dvimulf  15380  logbgt0b  15640  perfectlem2  15674  lgslem4  15682  lgsmod  15705  lgsdir2lem2  15708  lgsdir2  15712  lgsne0  15717  lgsmulsqcoprm  15725  lgseisenlem1  15749  2lgsoddprm  15792  2sqlem4  15797  wlk1walkdom  16070