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  566  bimsc1  907  biimp3a  1279  equsex  1660  euor  1971  euan  2001  cgsexg  2648  cgsex2g  2649  cgsex4g  2650  ceqsex  2651  sbciegft  2858  sbeqalb  2884  syl5sseq  3063  euotd  4054  ralxfr2d  4259  rexxfr2d  4260  nlimsucg  4354  wetriext  4364  relop  4553  resiexg  4723  iotass  4960  fnbr  5078  f1o00  5245  fnex  5474  foelrn  5486  acexmidlemab  5601  f1ocnv2d  5799  ofrval  5817  eloprabi  5917  1stconst  5937  2ndconst  5938  poxp  5948  smodm2  6008  smoiso  6015  nnsucuniel  6204  erth  6282  iinerm  6310  phplem4dom  6524  findcard2  6551  findcard2s  6552  fimax2gtrilemstep  6562  undifdcss  6579  supelti  6634  nlt1pig  6837  dfplpq2  6850  ltsonq  6894  archnqq  6913  nqnq0pi  6934  prarloclemn  6995  genprndl  7017  genprndu  7018  genpdisj  7019  addlocprlemgt  7030  addlocpr  7032  nqprl  7047  nqpru  7048  addnqprlemrl  7053  addnqprlemru  7054  mulnqprlemrl  7069  mulnqprlemru  7070  ltpopr  7091  ltexprlemloc  7103  ltexprlemrl  7106  cauappcvgprlemladdfu  7150  cauappcvgprlemladdfl  7151  caucvgprlemladdfu  7173  axcaucvglemres  7371  cnegex  7597  mullt0  7895  mulge0  8030  divap0  8083  div2negap  8134  prodgt0  8241  ltmul12a  8249  recgt1i  8287  div4p1lem1div2  8595  nn0lt2  8754  peano5uzti  8780  eluzp1m1  8967  eluzaddi  8970  eluzsubi  8971  uz2m1nn  9017  rphalflt  9088  ixxdisj  9246  iccgelb  9275  icodisj  9334  iccf1o  9346  fzsuc2  9416  fzonmapblen  9519  flqge0nn0  9621  flqge1nn  9622  modfzo0difsn  9723  expubnd  9903  bernneq  9963  bernneq2  9964  nn0opthlem2d  10018  facwordi  10037  bcpasc  10063  hashnncl  10093  recvguniq  10316  sqrt0rlem  10324  resqrexlemover  10331  resqrexlemcalc3  10337  resqrexlemgt0  10341  resqrexlemoverl  10342  recvalap  10418  nnabscl  10421  negfi  10545  climi0  10563  climge0  10598  isummolem3  10652  dvdslelemd  10711  dvdsleabs2  10714  mulmoddvds  10731  odd2np1  10740  oexpneg  10744  mod2eq1n2dvds  10746  sqoddm1div8z  10753  zsupcllemstep  10808  rplpwr  10883  rppwr  10884  nn0seqcvgd  10890  lcmneg  10923  qredeq  10945  dvdsnprmd  10974  oddprmge3  10983  oddpwdclemdvds  11015  oddpwdclemndvds  11016  oddpwdclemodd  11017  znege1  11023  qgt0numnn  11044  phibndlem  11059  hashgcdeq  11071