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  7541  recclnq  7760  nq0a0  7825  qreccl  10052  difelfzle  10552  exfzdc  10670  zsupcllemstep  10673  modifeq2int  10838  frec2uzlt2d  10856  zzlesq  11161  fihashgt0  11262  1elfz0hash  11263  lennncl  11340  wrdsymb0  11353  ccatsymb  11386  ccatlid  11390  ccatass  11392  ccatswrd  11458  swrdccat2  11459  ccatpfx  11489  swrdccatfn  11512  swrdccat  11523  caucvgrelemcau  11762  recvalap  11880  fzomaxdiflem  11895  2zsupmax  12009  2zinfmin  12028  fsumparts  12256  ntrivcvgap  12334  fsumdvds  12628  divconjdvds  12635  ndvdssub  12716  rplpwr  12823  dvdssqlem  12826  eucalgcvga  12855  mulgcddvds  12891  isprm2lem  12913  powm2modprm  13054  coprimeprodsq  13059  pythagtriplem11  13076  pythagtriplem13  13078  pcadd2  13143  4sqlem11  13203  grpidd  13756  ismndd  13803  gzsumwmhm  13856  mulgaddcom  14002  resghm  14116  conjnsg  14137  isrngd  14336  isringd  14430  01eq0ring  14580  lspsneq0b  14848  lmodindp1  14849  znf1o  15070  aspval  15099  psrgrp  15167  uniopn  15193  ntrval  15302  clsval  15303  neival  15335  restdis  15376  lmbrf  15407  cnpnei  15411  dviaddf  15897  dvimulf  15898  logbgt0b  16163  pellexlem2  16191  perfectlem2  16261  bposlem3  16274  lgslem4  16288  lgsmod  16311  lgsdir2lem2  16314  lgsdir2  16318  lgsne0  16323  lgsmulsqcoprm  16331  lgseisenlem1  16355  2lgsoddprm  16398  2sqlem4  16403  wlk1walkdom  16766  wlkreslem  16785