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  618  eqtr  2252  opabss  4179  euotd  4376  wetriext  4704  sosng  4828  xpsspw  4867  brcogw  4929  funimaexglem  5444  funfni  5463  fnco  5471  fnssres  5476  fn0  5483  fnimadisj  5484  fnimaeq0  5485  foco  5606  foimacnv  5637  fvelimab  5738  fvopab3ig  5756  dff3im  5827  dffo4  5830  fmptco  5848  f1eqcocnv  5970  f1ocnv2d  6267  f1o3d  6271  fnexALT  6313  elabreximd  6329  xp1st  6372  xp2nd  6373  tfrlemiubacc  6574  tfri2d  6580  tfr1onlemubacc  6590  tfrcllemubacc  6603  tfri3  6611  ecelqsg  6835  elqsn0m  6850  fidifsnen  7138  pr1or2  7504  recclnq  7723  nq0a0  7788  qreccl  9995  difelfzle  10493  exfzdc  10611  zsupcllemstep  10614  modifeq2int  10775  frec2uzlt2d  10793  zzlesq  11098  fihashgt0  11198  1elfz0hash  11199  lennncl  11272  wrdsymb0  11285  ccatsymb  11318  ccatlid  11322  ccatass  11324  ccatswrd  11390  swrdccat2  11391  ccatpfx  11421  swrdccatfn  11444  swrdccat  11455  caucvgrelemcau  11693  recvalap  11810  fzomaxdiflem  11825  2zsupmax  11939  2zinfmin  11956  fsumparts  12184  ntrivcvgap  12262  fsumdvds  12556  divconjdvds  12563  ndvdssub  12644  rplpwr  12751  dvdssqlem  12754  eucalgcvga  12783  mulgcddvds  12819  isprm2lem  12841  powm2modprm  12978  coprimeprodsq  12983  pythagtriplem11  13000  pythagtriplem13  13002  pcadd2  13067  4sqlem11  13127  grpidd  13649  ismndd  13701  gsumfzz  13753  gsumwmhm  13756  mulgaddcom  13902  resghm  14016  conjnsg  14037  isrngd  14195  isringd  14287  01eq0ring  14437  lspsneq0b  14704  lmodindp1  14705  znf1o  14928  psrgrp  14969  uniopn  14995  ntrval  15104  clsval  15105  neival  15137  restdis  15178  lmbrf  15209  cnpnei  15213  dviaddf  15699  dvimulf  15700  logbgt0b  15960  pellexlem2  15975  perfectlem2  15997  lgslem4  16005  lgsmod  16028  lgsdir2lem2  16031  lgsdir2  16035  lgsne0  16040  lgsmulsqcoprm  16048  lgseisenlem1  16072  2lgsoddprm  16115  2sqlem4  16120  wlk1walkdom  16483  wlkreslem  16502