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  614  eqtr  2207  opabss  4082  euotd  4272  wetriext  4594  sosng  4717  xpsspw  4756  brcogw  4814  funimaexglem  5318  funfni  5335  fnco  5343  fnssres  5348  fn0  5354  fnimadisj  5355  fnimaeq0  5356  foco  5467  foimacnv  5498  fvelimab  5592  fvopab3ig  5610  dff3im  5681  dffo4  5684  fmptco  5702  f1eqcocnv  5812  f1ocnv2d  6097  fnexALT  6135  xp1st  6189  xp2nd  6190  tfrlemiubacc  6354  tfri2d  6360  tfr1onlemubacc  6370  tfrcllemubacc  6383  tfri3  6391  ecelqsg  6613  elqsn0m  6628  fidifsnen  6897  recclnq  7420  nq0a0  7485  qreccl  9671  difelfzle  10163  exfzdc  10269  modifeq2int  10416  frec2uzlt2d  10434  zzlesq  10719  1elfz0hash  10817  caucvgrelemcau  11020  recvalap  11137  fzomaxdiflem  11152  2zsupmax  11265  2zinfmin  11282  fsumparts  11509  ntrivcvgap  11587  divconjdvds  11886  ndvdssub  11966  zsupcllemstep  11977  rplpwr  12059  dvdssqlem  12062  eucalgcvga  12089  mulgcddvds  12125  isprm2lem  12147  powm2modprm  12283  coprimeprodsq  12288  pythagtriplem11  12305  pythagtriplem13  12307  pcadd2  12372  4sqlem11  12432  grpidd  12856  ismndd  12895  mulgaddcom  13083  resghm  13196  conjnsg  13217  isrngd  13304  isringd  13392  01eq0ring  13533  lspsneq0b  13740  lmodindp1  13741  uniopn  13953  ntrval  14062  clsval  14063  neival  14095  restdis  14136  lmbrf  14167  cnpnei  14171  dviaddf  14621  dvimulf  14622  logbgt0b  14836  lgslem4  14857  lgsmod  14880  lgsdir2lem2  14883  lgsdir2  14887  lgsne0  14892  lgsmulsqcoprm  14900  lgseisenlem1  14903  2sqlem4  14918