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  456  eqtr  2102  opabss  3877  euotd  4055  wetriext  4365  sosng  4479  xpsspw  4518  brcogw  4573  funimaexglem  5062  funfni  5079  fnco  5087  fnssres  5092  fn0  5098  fnimadisj  5099  fnimaeq0  5100  foco  5206  foimacnv  5234  fvelimab  5323  fvopab3ig  5341  dff3im  5407  dffo4  5410  fmptco  5427  f1eqcocnv  5531  f1ocnv2d  5805  fnexALT  5841  xp1st  5893  xp2nd  5894  tfrlemiubacc  6049  tfri2d  6055  tfr1onlemubacc  6065  tfrcllemubacc  6078  tfri3  6086  ecelqsg  6297  elqsn0m  6312  fidifsnen  6538  recclnq  6895  nq0a0  6960  qreccl  9059  difelfzle  9473  exfzdc  9579  modifeq2int  9721  frec2uzlt2d  9739  1elfz0hash  10111  caucvgrelemcau  10309  recvalap  10426  fzomaxdiflem  10441  divconjdvds  10732  ndvdssub  10812  zsupcllemstep  10823  rplpwr  10898  dvdssqlem  10901  eucialgcvga  10922  mulgcddvds  10958  isprm2lem  10980