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  2249  opabss  4158  euotd  4353  wetriext  4681  sosng  4805  xpsspw  4844  brcogw  4905  funimaexglem  5420  funfni  5439  fnco  5447  fnssres  5452  fn0  5459  fnimadisj  5460  fnimaeq0  5461  foco  5579  foimacnv  5610  fvelimab  5711  fvopab3ig  5729  dff3im  5800  dffo4  5803  fmptco  5821  f1eqcocnv  5942  f1ocnv2d  6237  fnexALT  6282  xp1st  6337  xp2nd  6338  tfrlemiubacc  6539  tfri2d  6545  tfr1onlemubacc  6555  tfrcllemubacc  6568  tfri3  6576  ecelqsg  6800  elqsn0m  6815  fidifsnen  7100  pr1or2  7459  recclnq  7672  nq0a0  7737  qreccl  9937  difelfzle  10431  exfzdc  10549  zsupcllemstep  10552  modifeq2int  10711  frec2uzlt2d  10729  zzlesq  11033  fihashgt0  11132  1elfz0hash  11133  lennncl  11199  wrdsymb0  11212  ccatsymb  11245  ccatlid  11249  ccatass  11251  ccatswrd  11317  swrdccat2  11318  ccatpfx  11348  swrdccatfn  11371  swrdccat  11382  caucvgrelemcau  11620  recvalap  11737  fzomaxdiflem  11752  2zsupmax  11866  2zinfmin  11883  fsumparts  12111  ntrivcvgap  12189  fsumdvds  12483  divconjdvds  12490  ndvdssub  12571  rplpwr  12678  dvdssqlem  12681  eucalgcvga  12710  mulgcddvds  12746  isprm2lem  12768  powm2modprm  12905  coprimeprodsq  12910  pythagtriplem11  12927  pythagtriplem13  12929  pcadd2  12994  4sqlem11  13054  grpidd  13546  ismndd  13600  gsumfzz  13658  gsumwmhm  13661  mulgaddcom  13813  resghm  13927  conjnsg  13948  isrngd  14047  isringd  14135  01eq0ring  14284  lspsneq0b  14523  lmodindp1  14524  znf1o  14747  psrgrp  14786  uniopn  14812  ntrval  14921  clsval  14922  neival  14954  restdis  14995  lmbrf  15026  cnpnei  15030  dviaddf  15516  dvimulf  15517  logbgt0b  15777  pellexlem2  15792  perfectlem2  15814  lgslem4  15822  lgsmod  15845  lgsdir2lem2  15848  lgsdir2  15852  lgsne0  15857  lgsmulsqcoprm  15865  lgseisenlem1  15889  2lgsoddprm  15932  2sqlem4  15937  wlk1walkdom  16300  wlkreslem  16319