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  379  bitr  463  eqtr  2157  opabss  3992  euotd  4176  wetriext  4491  sosng  4612  xpsspw  4651  brcogw  4708  funimaexglem  5206  funfni  5223  fnco  5231  fnssres  5236  fn0  5242  fnimadisj  5243  fnimaeq0  5244  foco  5355  foimacnv  5385  fvelimab  5477  fvopab3ig  5495  dff3im  5565  dffo4  5568  fmptco  5586  f1eqcocnv  5692  f1ocnv2d  5974  fnexALT  6011  xp1st  6063  xp2nd  6064  tfrlemiubacc  6227  tfri2d  6233  tfr1onlemubacc  6243  tfrcllemubacc  6256  tfri3  6264  ecelqsg  6482  elqsn0m  6497  fidifsnen  6764  recclnq  7200  nq0a0  7265  qreccl  9434  difelfzle  9911  exfzdc  10017  modifeq2int  10159  frec2uzlt2d  10177  1elfz0hash  10552  caucvgrelemcau  10752  recvalap  10869  fzomaxdiflem  10884  2zsupmax  10997  fsumparts  11239  ntrivcvgap  11317  divconjdvds  11547  ndvdssub  11627  zsupcllemstep  11638  rplpwr  11715  dvdssqlem  11718  eucalgcvga  11739  mulgcddvds  11775  isprm2lem  11797  uniopn  12168  ntrval  12279  clsval  12280  neival  12312  restdis  12353  lmbrf  12384  cnpnei  12388  dviaddf  12838  dvimulf  12839