Theorem biimparc 504

Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimparc	|- ( ( ch /\ ph ) -> ps )

Proof of Theorem biimparc

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimprcd 240	. 2 |- ( ch -> ( ph -> ps ) )
3	2	imp 445	1 |- ( ( ch /\ ph ) -> ps )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  biantr  972  elrab3t  3362  difprsnss  4329  elpw2g  4827  ideqg  5273  elrnmpt1s  5373  elrnmptg  5375  eqfnfv2  6312  fmpt  6381  elunirn  6509  fun11iun  7126  tposfo2  7375  tposf12  7377  dom2lem  7995  enfii  8177  ssnnfi  8179  ac6sfi  8204  unfilem1  8224  inf3lem2  8526  infdiffi  8555  dfac5lem5  8950  dfac2  8953  dfac12k  8969  cfslb2n  9090  enfin2i  9143  fin23lem19  9158  axdc2lem  9270  axdc3lem4  9275  winainflem  9515  indpi  9729  ltexnq  9797  ltbtwnnq  9800  ltexprlem6  9863  prlem936  9869  elreal2  9953  fimaxre3  10970  addmodlteq  12745  expnbnd  12993  opfi1uzind  13283  opfi1uzindOLD  13289  repswswrd  13531  climcnds  14583  fprod2dlem  14710  fprodle  14727  unbenlem  15612  acsfn  16320  lsmcv  19141  maducoeval2  20446  bastop2  20798  neipeltop  20933  rnelfmlem  21756  isfcls  21813  tgphaus  21920  mbfi1fseqlem4  23485  ulm2  24139  lgsqrmodndvds  25078  2lgsoddprm  25141  ax5seglem5  25813  wlkdlem4  26582  wlknwwlksnsur  26776  3wlkdlem4  27022  spanunsni  28438  nonbooli  28510  nmopun  28873  lncnopbd  28896  pjnmopi  29007  sumdmdlem  29277  spc2ed  29312  disjun0  29408  rnmpt2ss  29473  esumpcvgval  30140  bnj545  30965  bnj900  30999  bnj1498  31129  soseq  31751  btwnconn1lem7  32200  ivthALT  32330  topfneec  32350  bj-snglss  32958  bj-ismoored  33062  mptsnunlem  33185  icoreresf  33200  lindsenlbs  33404  matunitlindf  33407  poimirlem14  33423  poimirlem22  33431  poimirlem26  33435  poimirlem29  33438  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  fdc  33541  ismtyres  33607  isdrngo3  33758  lshpset2N  34406  3dimlem1  34744  3dim3  34755  cdleme31fv2  35681  isnumbasgrplem3  37675  pm13.13b  38609  ax6e2ndeqALT  39167  sineq0ALT  39173  elrnmpt1sf  39376  nn0sumshdiglemB  42414