Theorem biimpar 297

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exbiri  382  bitr  472  biadanid  614  eqtr  2225  opabss  4124  euotd  4317  wetriext  4643  sosng  4766  xpsspw  4805  brcogw  4865  funimaexglem  5376  funfni  5395  fnco  5403  fnssres  5408  fn0  5415  fnimadisj  5416  fnimaeq0  5417  foco  5531  foimacnv  5562  fvelimab  5658  fvopab3ig  5676  dff3im  5748  dffo4  5751  fmptco  5769  f1eqcocnv  5883  f1ocnv2d  6173  fnexALT  6219  xp1st  6274  xp2nd  6275  tfrlemiubacc  6439  tfri2d  6445  tfr1onlemubacc  6455  tfrcllemubacc  6468  tfri3  6476  ecelqsg  6698  elqsn0m  6713  fidifsnen  6993  pr1or2  7328  recclnq  7540  nq0a0  7605  qreccl  9798  difelfzle  10291  exfzdc  10406  zsupcllemstep  10409  modifeq2int  10568  frec2uzlt2d  10586  zzlesq  10890  1elfz0hash  10988  lennncl  11051  wrdsymb0  11063  ccatsymb  11096  ccatlid  11100  ccatass  11102  ccatswrd  11161  swrdccat2  11162  ccatpfx  11192  swrdccatfn  11215  swrdccat  11226  caucvgrelemcau  11406  recvalap  11523  fzomaxdiflem  11538  2zsupmax  11652  2zinfmin  11669  fsumparts  11896  ntrivcvgap  11974  fsumdvds  12268  divconjdvds  12275  ndvdssub  12356  rplpwr  12463  dvdssqlem  12466  eucalgcvga  12495  mulgcddvds  12531  isprm2lem  12553  powm2modprm  12690  coprimeprodsq  12695  pythagtriplem11  12712  pythagtriplem13  12714  pcadd2  12779  4sqlem11  12839  grpidd  13330  ismndd  13384  gsumfzz  13442  gsumwmhm  13445  mulgaddcom  13597  resghm  13711  conjnsg  13732  isrngd  13830  isringd  13918  01eq0ring  14066  lspsneq0b  14304  lmodindp1  14305  znf1o  14528  psrgrp  14562  uniopn  14588  ntrval  14697  clsval  14698  neival  14730  restdis  14771  lmbrf  14802  cnpnei  14806  dviaddf  15292  dvimulf  15293  logbgt0b  15553  perfectlem2  15587  lgslem4  15595  lgsmod  15618  lgsdir2lem2  15621  lgsdir2  15625  lgsne0  15630  lgsmulsqcoprm  15638  lgseisenlem1  15662  2lgsoddprm  15705  2sqlem4  15710