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  2223  opabss  4109  euotd  4300  wetriext  4626  sosng  4749  xpsspw  4788  brcogw  4848  funimaexglem  5358  funfni  5377  fnco  5385  fnssres  5390  fn0  5397  fnimadisj  5398  fnimaeq0  5399  foco  5511  foimacnv  5542  fvelimab  5637  fvopab3ig  5655  dff3im  5727  dffo4  5730  fmptco  5748  f1eqcocnv  5862  f1ocnv2d  6152  fnexALT  6198  xp1st  6253  xp2nd  6254  tfrlemiubacc  6418  tfri2d  6424  tfr1onlemubacc  6434  tfrcllemubacc  6447  tfri3  6455  ecelqsg  6677  elqsn0m  6692  fidifsnen  6969  recclnq  7507  nq0a0  7572  qreccl  9765  difelfzle  10258  exfzdc  10371  zsupcllemstep  10374  modifeq2int  10533  frec2uzlt2d  10551  zzlesq  10855  1elfz0hash  10953  lennncl  11016  wrdsymb0  11028  ccatsymb  11061  ccatlid  11065  ccatass  11067  ccatswrd  11126  swrdccat2  11127  ccatpfx  11155  caucvgrelemcau  11324  recvalap  11441  fzomaxdiflem  11456  2zsupmax  11570  2zinfmin  11587  fsumparts  11814  ntrivcvgap  11892  fsumdvds  12186  divconjdvds  12193  ndvdssub  12274  rplpwr  12381  dvdssqlem  12384  eucalgcvga  12413  mulgcddvds  12449  isprm2lem  12471  powm2modprm  12608  coprimeprodsq  12613  pythagtriplem11  12630  pythagtriplem13  12632  pcadd2  12697  4sqlem11  12757  grpidd  13248  ismndd  13302  gsumfzz  13360  gsumwmhm  13363  mulgaddcom  13515  resghm  13629  conjnsg  13650  isrngd  13748  isringd  13836  01eq0ring  13984  lspsneq0b  14222  lmodindp1  14223  znf1o  14446  psrgrp  14480  uniopn  14506  ntrval  14615  clsval  14616  neival  14648  restdis  14689  lmbrf  14720  cnpnei  14724  dviaddf  15210  dvimulf  15211  logbgt0b  15471  perfectlem2  15505  lgslem4  15513  lgsmod  15536  lgsdir2lem2  15539  lgsdir2  15543  lgsne0  15548  lgsmulsqcoprm  15556  lgseisenlem1  15580  2lgsoddprm  15623  2sqlem4  15628