Theorem biimpa 294

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  simprbda  380  simplbda  381  pm5.1  590  bimsc1  947  biimp3a  1323  equsex  1706  euor  2025  euan  2055  cgsexg  2721  cgsex2g  2722  cgsex4g  2723  ceqsex  2724  sbciegft  2939  sbeqalb  2965  sseqtrid  3147  exmidn0m  4124  euotd  4176  ralxfr2d  4385  rexxfr2d  4386  nlimsucg  4481  wetriext  4491  relop  4689  resiexg  4864  iotass  5105  fnbr  5225  f1o00  5402  fnex  5642  foelrn  5654  acexmidlemab  5768  f1ocnv2d  5974  ofrval  5992  eloprabi  6094  1stconst  6118  2ndconst  6119  poxp  6129  smodm2  6192  smoiso  6199  nnsucuniel  6391  erth  6473  iinerm  6501  phplem4dom  6756  findcard2  6783  findcard2s  6784  fimax2gtrilemstep  6794  undifdcss  6811  fipwssg  6867  supelti  6889  nlt1pig  7149  dfplpq2  7162  ltsonq  7206  archnqq  7225  nqnq0pi  7246  prarloclemn  7307  genprndl  7329  genprndu  7330  genpdisj  7331  addlocprlemgt  7342  addlocpr  7344  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  mulnqprlemrl  7381  mulnqprlemru  7382  ltpopr  7403  ltexprlemloc  7415  ltexprlemrl  7418  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  caucvgprlemladdfu  7485  suplocexprlemru  7527  axcaucvglemres  7707  cnegex  7940  mullt0  8242  eqord1  8245  mulge0  8381  divap0  8444  div2negap  8495  prodgt0  8610  ltmul12a  8618  recgt1i  8656  div4p1lem1div2  8973  nn0lt2  9132  peano5uzti  9159  btwnapz  9181  eluzp1m1  9349  eluzaddi  9352  eluzsubi  9353  uz2m1nn  9399  rphalflt  9471  xleaddadd  9670  ixxdisj  9686  iccgelb  9715  icodisj  9775  iccf1o  9787  fzsuc2  9859  fzonmapblen  9964  flqge0nn0  10066  flqge1nn  10067  modfzo0difsn  10168  expubnd  10350  bernneq  10412  bernneq2  10413  nn0opthlem2d  10467  facwordi  10486  bcpasc  10512  hashnncl  10542  recvguniq  10767  sqrt0rlem  10775  resqrexlemover  10782  resqrexlemcalc3  10788  resqrexlemgt0  10792  resqrexlemoverl  10793  recvalap  10869  nnabscl  10872  negfi  10999  climi0  11058  climge0  11094  summodclem3  11149  fsumsplit  11176  fisumcom2  11207  fisumrev2  11215  explecnv  11274  cvgratnnlemseq  11295  eftlub  11396  sin02gt0  11470  dvdslelemd  11541  dvdsleabs2  11544  mulmoddvds  11561  odd2np1  11570  oexpneg  11574  mod2eq1n2dvds  11576  sqoddm1div8z  11583  zsupcllemstep  11638  rplpwr  11715  rppwr  11716  nn0seqcvgd  11722  lcmneg  11755  qredeq  11777  dvdsnprmd  11806  oddprmge3  11815  oddpwdclemdvds  11848  oddpwdclemndvds  11849  oddpwdclemodd  11850  znege1  11856  qgt0numnn  11877  phibndlem  11892  hashgcdeq  11904  ennnfonelemf1  11931  neiuni  12330  neissex  12334  tgrest  12338  tgcnp  12378  lmfpm  12412  lmcl  12414  lmss  12415  lmff  12418  psmetdmdm  12493  xmeter  12605  neibl  12660  xmettxlem  12678  tgqioo  12716  cnopnap  12763  limcimo  12803  sinq12gt0  12911  isomninnlem  13225