Theorem biimpa 280

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

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  simprbda  365  simplbda  366  pm5.1  533  bimsc1  870  biimp3a  1235  equsex  1616  euor  1926  euan  1956  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  ceqsex  2592  sbciegft  2793  sbeqalb  2815  syl5sseq  2993  euotd  3991  ralxfr2d  4196  rexxfr2d  4197  nlimsucg  4290  wetriext  4301  relop  4486  resiexg  4653  iotass  4884  fnbr  5001  f1o00  5161  fnex  5383  acexmidlemab  5506  f1ocnv2d  5704  ofrval  5722  eloprabi  5822  1stconst  5842  2ndconst  5843  poxp  5853  smodm2  5910  smoiso  5917  erth  6150  iinerm  6178  phplem4dom  6324  findcard2  6346  findcard2s  6347  nlt1pig  6439  dfplpq2  6452  ltsonq  6496  archnqq  6515  nqnq0pi  6536  prarloclemn  6597  genprndl  6619  genprndu  6620  genpdisj  6621  addlocprlemgt  6632  addlocpr  6634  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  mulnqprlemrl  6671  mulnqprlemru  6672  ltpopr  6693  ltexprlemloc  6705  ltexprlemrl  6708  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemladdfu  6775  axcaucvglemres  6973  cnegex  7189  mullt0  7475  mulge0  7610  divap0  7663  div2negap  7711  prodgt0  7818  ltmul12a  7826  recgt1i  7864  div4p1lem1div2  8177  nn0lt2  8322  peano5uzti  8346  eluzp1m1  8496  eluzaddi  8499  eluzsubi  8500  uz2m1nn  8542  rphalflt  8612  ixxdisj  8772  iccgelb  8801  icodisj  8860  iccf1o  8872  fzsuc2  8941  fzonmapblen  9043  flqge0nn0  9135  flqge1nn  9136  expubnd  9311  bernneq  9369  bernneq2  9370  recvguniq  9593  sqrt0rlem  9601  resqrexlemover  9608  resqrexlemcalc3  9614  resqrexlemgt0  9618  resqrexlemoverl  9619  recvalap  9693  nnabscl  9696  climi0  9810  climge0  9845  nn0seqcvgd  9880