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  9992  difelfzle  10490  exfzdc  10608  zsupcllemstep  10611  modifeq2int  10772  frec2uzlt2d  10790  zzlesq  11095  fihashgt0  11195  1elfz0hash  11196  lennncl  11269  wrdsymb0  11282  ccatsymb  11315  ccatlid  11319  ccatass  11321  ccatswrd  11387  swrdccat2  11388  ccatpfx  11418  swrdccatfn  11441  swrdccat  11452  caucvgrelemcau  11690  recvalap  11807  fzomaxdiflem  11822  2zsupmax  11936  2zinfmin  11953  fsumparts  12181  ntrivcvgap  12259  fsumdvds  12553  divconjdvds  12560  ndvdssub  12641  rplpwr  12748  dvdssqlem  12751  eucalgcvga  12780  mulgcddvds  12816  isprm2lem  12838  powm2modprm  12975  coprimeprodsq  12980  pythagtriplem11  12997  pythagtriplem13  12999  pcadd2  13064  4sqlem11  13124  grpidd  13646  ismndd  13698  gsumfzz  13750  gsumwmhm  13753  mulgaddcom  13899  resghm  14013  conjnsg  14034  isrngd  14192  isringd  14284  01eq0ring  14434  lspsneq0b  14701  lmodindp1  14702  znf1o  14925  psrgrp  14966  uniopn  14992  ntrval  15101  clsval  15102  neival  15134  restdis  15175  lmbrf  15206  cnpnei  15210  dviaddf  15696  dvimulf  15697  logbgt0b  15957  pellexlem2  15972  perfectlem2  15994  lgslem4  16002  lgsmod  16025  lgsdir2lem2  16028  lgsdir2  16032  lgsne0  16037  lgsmulsqcoprm  16045  lgseisenlem1  16069  2lgsoddprm  16112  2sqlem4  16117  wlk1walkdom  16480  wlkreslem  16499