Theorem biimpar 291

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  exbiri  374  bitr  455  eqtr  2098  opabss  3842  euotd  4009  wetriext  4319  sosng  4431  xpsspw  4468  brcogw  4522  funimaexglem  5002  funfni  5019  fnco  5027  fnssres  5032  fn0  5038  fnimadisj  5039  fnimaeq0  5040  foco  5136  foimacnv  5164  fvelimab  5250  fvopab3ig  5267  dff3im  5333  dffo4  5336  fmptco  5351  f1eqcocnv  5451  f1ocnv2d  5724  fnexALT  5760  xp1st  5812  xp2nd  5813  tfrlemiubacc  5967  tfri2d  5973  tfri3  5976  ecelqsg  6182  elqsn0m  6197  fidifsnen  6355  recclnq  6582  nq0a0  6647  qreccl  8727  difelfzle  9145  exfzdc  9249  modifeq2int  9388  frec2uzlt2d  9406  caucvgrelemcau  9866  recvalap  9983  fzomaxdiflem  9998  divconjdvds  10249  ndvdssub  10330  zsupcllemstep  10341  rplpwr  10416  dvdssqlem  10419  eucialgcvga  10440  mulgcddvds  10476  isprm2lem  10498