Theorem biimpa 290

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

Hypothesis

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

Assertion

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

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 142	. 2 |- ( ph -> ( ps -> ch ) )
3	2	imp 122	1 |- ( ( ph /\ ps ) -> ch )

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  simprbda  375  simplbda  376  pm5.1  565  bimsc1  904  biimp3a  1276  equsex  1656  euor  1967  euan  1997  cgsexg  2634  cgsex2g  2635  cgsex4g  2636  ceqsex  2637  sbciegft  2844  sbeqalb  2870  syl5sseq  3047  euotd  4009  ralxfr2d  4214  rexxfr2d  4215  nlimsucg  4309  wetriext  4319  relop  4504  resiexg  4673  iotass  4904  fnbr  5021  f1o00  5181  fnex  5404  acexmidlemab  5526  f1ocnv2d  5724  ofrval  5742  eloprabi  5842  1stconst  5862  2ndconst  5863  poxp  5873  smodm2  5933  smoiso  5940  erth  6173  iinerm  6201  phplem4dom  6348  findcard2  6373  findcard2s  6374  supelti  6415  nlt1pig  6531  dfplpq2  6544  ltsonq  6588  archnqq  6607  nqnq0pi  6628  prarloclemn  6689  genprndl  6711  genprndu  6712  genpdisj  6713  addlocprlemgt  6724  addlocpr  6726  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  mulnqprlemrl  6763  mulnqprlemru  6764  ltpopr  6785  ltexprlemloc  6797  ltexprlemrl  6800  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  caucvgprlemladdfu  6867  axcaucvglemres  7065  cnegex  7286  mullt0  7584  mulge0  7719  divap0  7772  div2negap  7823  prodgt0  7930  ltmul12a  7938  recgt1i  7976  div4p1lem1div2  8284  nn0lt2  8429  peano5uzti  8455  eluzp1m1  8642  eluzaddi  8645  eluzsubi  8646  uz2m1nn  8692  rphalflt  8763  ixxdisj  8926  iccgelb  8955  icodisj  9014  iccf1o  9026  fzsuc2  9096  fzonmapblen  9196  flqge0nn0  9295  flqge1nn  9296  modfzo0difsn  9397  expubnd  9533  bernneq  9593  bernneq2  9594  nn0opthlem2d  9648  facwordi  9667  bcpasc  9693  recvguniq  9881  sqrt0rlem  9889  resqrexlemover  9896  resqrexlemcalc3  9902  resqrexlemgt0  9906  resqrexlemoverl  9907  recvalap  9983  nnabscl  9986  negfi  10110  climi0  10128  climge0  10163  dvdslelemd  10243  dvdsleabs2  10246  mulmoddvds  10263  odd2np1  10272  oexpneg  10276  mod2eq1n2dvds  10279  sqoddm1div8z  10286  zsupcllemstep  10341  rplpwr  10416  rppwr  10417  nn0seqcvgd  10423  lcmneg  10456  qredeq  10478  dvdsnprmd  10507  oddprmge3  10516  oddpwdclemdvds  10548  oddpwdclemndvds  10549  oddpwdclemodd  10550  znege1  10556