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  2183  opabss  4045  euotd  4231  wetriext  4553  sosng  4676  xpsspw  4715  brcogw  4772  funimaexglem  5270  funfni  5287  fnco  5295  fnssres  5300  fn0  5306  fnimadisj  5307  fnimaeq0  5308  foco  5419  foimacnv  5449  fvelimab  5541  fvopab3ig  5559  dff3im  5629  dffo4  5632  fmptco  5650  f1eqcocnv  5758  f1ocnv2d  6041  fnexALT  6078  xp1st  6130  xp2nd  6131  tfrlemiubacc  6294  tfri2d  6300  tfr1onlemubacc  6310  tfrcllemubacc  6323  tfri3  6331  ecelqsg  6550  elqsn0m  6565  fidifsnen  6832  recclnq  7329  nq0a0  7394  qreccl  9576  difelfzle  10065  exfzdc  10171  modifeq2int  10317  frec2uzlt2d  10335  1elfz0hash  10715  caucvgrelemcau  10918  recvalap  11035  fzomaxdiflem  11050  2zsupmax  11163  2zinfmin  11180  fsumparts  11407  ntrivcvgap  11485  divconjdvds  11783  ndvdssub  11863  zsupcllemstep  11874  rplpwr  11956  dvdssqlem  11959  eucalgcvga  11986  mulgcddvds  12022  isprm2lem  12044  powm2modprm  12180  coprimeprodsq  12185  pythagtriplem11  12202  pythagtriplem13  12204  uniopn  12599  ntrval  12710  clsval  12711  neival  12743  restdis  12784  lmbrf  12815  cnpnei  12819  dviaddf  13269  dvimulf  13270  logbgt0b  13484  lgslem4  13504  lgsmod  13527  lgsdir2lem2  13530  lgsdir2  13534  lgsne0  13539  lgsmulsqcoprm  13547  2sqlem4  13554