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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  exbiri  382  bitr  476  biadanid  622  eqtr  2256  opabss  4195  euotd  4395  wetriext  4724  sosng  4848  xpsspw  4887  brcogw  4949  funimaexglem  5464  funfni  5483  fnco  5491  fnssres  5496  fn0  5503  fnimadisj  5504  fnimaeq0  5505  foco  5626  foimacnv  5657  fvelimab  5759  fvopab3ig  5779  dff3im  5853  dffo4  5856  fmptco  5874  f1eqcocnv  5997  f1ocnv2d  6294  f1o3d  6298  fnexALT  6340  elabreximd  6356  xp1st  6399  xp2nd  6400  tfrlemiubacc  6601  tfri2d  6607  tfr1onlemubacc  6617  tfrcllemubacc  6630  tfri3  6638  ecelqsg  6862  elqsn0m  6877  fidifsnen  7172  pr1or2  7540  recclnq  7759  nq0a0  7824  qreccl  10042  difelfzle  10541  exfzdc  10659  zsupcllemstep  10662  modifeq2int  10823  frec2uzlt2d  10841  zzlesq  11146  fihashgt0  11246  1elfz0hash  11247  lennncl  11324  wrdsymb0  11337  ccatsymb  11370  ccatlid  11374  ccatass  11376  ccatswrd  11442  swrdccat2  11443  ccatpfx  11473  swrdccatfn  11496  swrdccat  11507  caucvgrelemcau  11746  recvalap  11863  fzomaxdiflem  11878  2zsupmax  11992  2zinfmin  12009  fsumparts  12237  ntrivcvgap  12315  fsumdvds  12609  divconjdvds  12616  ndvdssub  12697  rplpwr  12804  dvdssqlem  12807  eucalgcvga  12836  mulgcddvds  12872  isprm2lem  12894  powm2modprm  13031  coprimeprodsq  13036  pythagtriplem11  13053  pythagtriplem13  13055  pcadd2  13120  4sqlem11  13180  grpidd  13703  ismndd  13750  gzsumwmhm  13803  mulgaddcom  13949  resghm  14063  conjnsg  14084  isrngd  14252  isringd  14346  01eq0ring  14496  lspsneq0b  14764  lmodindp1  14765  znf1o  14986  aspval  15015  psrgrp  15076  uniopn  15102  ntrval  15211  clsval  15212  neival  15244  restdis  15285  lmbrf  15316  cnpnei  15320  dviaddf  15806  dvimulf  15807  logbgt0b  16068  pellexlem2  16092  perfectlem2  16114  lgslem4  16122  lgsmod  16145  lgsdir2lem2  16148  lgsdir2  16152  lgsne0  16157  lgsmulsqcoprm  16165  lgseisenlem1  16189  2lgsoddprm  16232  2sqlem4  16237  wlk1walkdom  16600  wlkreslem  16619