Theorem biimpar 295

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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exbiri  380  bitr  464  eqtr  2175  opabss  4028  euotd  4213  wetriext  4534  sosng  4656  xpsspw  4695  brcogw  4752  funimaexglem  5250  funfni  5267  fnco  5275  fnssres  5280  fn0  5286  fnimadisj  5287  fnimaeq0  5288  foco  5399  foimacnv  5429  fvelimab  5521  fvopab3ig  5539  dff3im  5609  dffo4  5612  fmptco  5630  f1eqcocnv  5736  f1ocnv2d  6018  fnexALT  6055  xp1st  6107  xp2nd  6108  tfrlemiubacc  6271  tfri2d  6277  tfr1onlemubacc  6287  tfrcllemubacc  6300  tfri3  6308  ecelqsg  6526  elqsn0m  6541  fidifsnen  6808  recclnq  7295  nq0a0  7360  qreccl  9533  difelfzle  10015  exfzdc  10121  modifeq2int  10267  frec2uzlt2d  10285  1elfz0hash  10662  caucvgrelemcau  10862  recvalap  10979  fzomaxdiflem  10994  2zsupmax  11107  fsumparts  11349  ntrivcvgap  11427  divconjdvds  11722  ndvdssub  11802  zsupcllemstep  11813  rplpwr  11891  dvdssqlem  11894  eucalgcvga  11915  mulgcddvds  11951  isprm2lem  11973  uniopn  12359  ntrval  12470  clsval  12471  neival  12503  restdis  12544  lmbrf  12575  cnpnei  12579  dviaddf  13029  dvimulf  13030  logbgt0b  13243