Theorem biimpar 293

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 157	. 2 |- ( ph -> ( ch -> ps ) )
3	2	imp 123	1 |- ( ( ph /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exbiri  377  bitr  461  eqtr  2132  opabss  3952  euotd  4136  wetriext  4451  sosng  4572  xpsspw  4611  brcogw  4668  funimaexglem  5164  funfni  5181  fnco  5189  fnssres  5194  fn0  5200  fnimadisj  5201  fnimaeq0  5202  foco  5313  foimacnv  5341  fvelimab  5431  fvopab3ig  5449  dff3im  5519  dffo4  5522  fmptco  5540  f1eqcocnv  5646  f1ocnv2d  5928  fnexALT  5965  xp1st  6017  xp2nd  6018  tfrlemiubacc  6181  tfri2d  6187  tfr1onlemubacc  6197  tfrcllemubacc  6210  tfri3  6218  ecelqsg  6436  elqsn0m  6451  fidifsnen  6717  recclnq  7148  nq0a0  7213  qreccl  9336  difelfzle  9804  exfzdc  9910  modifeq2int  10052  frec2uzlt2d  10070  1elfz0hash  10445  caucvgrelemcau  10644  recvalap  10761  fzomaxdiflem  10776  2zsupmax  10889  fsumparts  11131  divconjdvds  11395  ndvdssub  11475  zsupcllemstep  11486  rplpwr  11561  dvdssqlem  11564  eucalgcvga  11585  mulgcddvds  11621  isprm2lem  11643  uniopn  12011  ntrval  12122  clsval  12123  neival  12155  restdis  12196  lmbrf  12226  cnpnei  12230  dviaddf  12624  dvimulf  12625