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  5561  foimacnv  5592  fvelimab  5692  fvopab3ig  5710  dff3im  5782  dffo4  5785  fmptco  5803  f1eqcocnv  5921  f1ocnv2d  6216  fnexALT  6262  xp1st  6317  xp2nd  6318  tfrlemiubacc  6482  tfri2d  6488  tfr1onlemubacc  6498  tfrcllemubacc  6511  tfri3  6519  ecelqsg  6743  elqsn0m  6758  fidifsnen  7040  pr1or2  7378  recclnq  7590  nq0a0  7655  qreccl  9849  difelfzle  10342  exfzdc  10458  zsupcllemstep  10461  modifeq2int  10620  frec2uzlt2d  10638  zzlesq  10942  fihashgt0  11040  1elfz0hash  11041  lennncl  11104  wrdsymb0  11117  ccatsymb  11150  ccatlid  11154  ccatass  11156  ccatswrd  11218  swrdccat2  11219  ccatpfx  11249  swrdccatfn  11272  swrdccat  11283  caucvgrelemcau  11507  recvalap  11624  fzomaxdiflem  11639  2zsupmax  11753  2zinfmin  11770  fsumparts  11997  ntrivcvgap  12075  fsumdvds  12369  divconjdvds  12376  ndvdssub  12457  rplpwr  12564  dvdssqlem  12567  eucalgcvga  12596  mulgcddvds  12632  isprm2lem  12654  powm2modprm  12791  coprimeprodsq  12796  pythagtriplem11  12813  pythagtriplem13  12815  pcadd2  12880  4sqlem11  12940  grpidd  13432  ismndd  13486  gsumfzz  13544  gsumwmhm  13547  mulgaddcom  13699  resghm  13813  conjnsg  13834  isrngd  13932  isringd  14020  01eq0ring  14169  lspsneq0b  14407  lmodindp1  14408  znf1o  14631  psrgrp  14665  uniopn  14691  ntrval  14800  clsval  14801  neival  14833  restdis  14874  lmbrf  14905  cnpnei  14909  dviaddf  15395  dvimulf  15396  logbgt0b  15656  perfectlem2  15690  lgslem4  15698  lgsmod  15721  lgsdir2lem2  15724  lgsdir2  15728  lgsne0  15733  lgsmulsqcoprm  15741  lgseisenlem1  15765  2lgsoddprm  15808  2sqlem4  15813  wlk1walkdom  16105  wlkreslem  16122