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  10051  difelfzle  10551  exfzdc  10669  zsupcllemstep  10672  modifeq2int  10836  frec2uzlt2d  10854  zzlesq  11159  fihashgt0  11260  1elfz0hash  11261  lennncl  11338  wrdsymb0  11351  ccatsymb  11384  ccatlid  11388  ccatass  11390  ccatswrd  11456  swrdccat2  11457  ccatpfx  11487  swrdccatfn  11510  swrdccat  11521  caucvgrelemcau  11760  recvalap  11878  fzomaxdiflem  11893  2zsupmax  12007  2zinfmin  12025  fsumparts  12253  ntrivcvgap  12331  fsumdvds  12625  divconjdvds  12632  ndvdssub  12713  rplpwr  12820  dvdssqlem  12823  eucalgcvga  12852  mulgcddvds  12888  isprm2lem  12910  powm2modprm  13051  coprimeprodsq  13056  pythagtriplem11  13073  pythagtriplem13  13075  pcadd2  13140  4sqlem11  13200  grpidd  13752  ismndd  13799  gzsumwmhm  13852  mulgaddcom  13998  resghm  14112  conjnsg  14133  isrngd  14301  isringd  14395  01eq0ring  14545  lspsneq0b  14813  lmodindp1  14814  znf1o  15035  aspval  15064  psrgrp  15125  uniopn  15151  ntrval  15260  clsval  15261  neival  15293  restdis  15334  lmbrf  15365  cnpnei  15369  dviaddf  15855  dvimulf  15856  logbgt0b  16121  pellexlem2  16149  perfectlem2  16198  bposlem3  16211  lgslem4  16220  lgsmod  16243  lgsdir2lem2  16246  lgsdir2  16250  lgsne0  16255  lgsmulsqcoprm  16263  lgseisenlem1  16287  2lgsoddprm  16330  2sqlem4  16335  wlk1walkdom  16698  wlkreslem  16717