Theorem biimpa 296

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117

This theorem is used by:  simprbda  383  simplbda  384  pm5.1  609  biadanid  622  bimsc1  976  biimp3a  1386  equsex  1780  euor  2112  euan  2143  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  ceqsex  2860  sbciegft  3082  sbeqalb  3108  sseqtrid  3298  exmidn0m  4340  euotd  4397  ralxfr2d  4612  rexxfr2d  4613  nlimsucg  4715  wetriext  4726  relop  4932  resiexg  5111  iotass  5358  fnbr  5488  f1o00  5679  foelcdmi  5758  fnex  5940  foelrn  5961  riotaeqimp  6066  acexmidlemab  6082  f1ocnv2d  6297  f1o3d  6301  ofrval  6317  elabreximd  6360  eloprabi  6436  1stconst  6461  2ndconst  6462  poxp  6472  smodm2  6571  smoiso  6578  nnsucuniel  6773  erth  6858  iinerm  6886  pw2f1odclem  7140  pw2f1odc  7141  phplem4dom  7169  findcard2  7199  findcard2s  7200  fimax2gtrilemstep  7211  undifdcss  7236  tpfidceq  7243  fipwssg  7318  2omap  7324  supelti  7348  nlt1pig  7714  dfplpq2  7727  ltsonq  7771  archnqq  7790  nqnq0pi  7811  prarloclemn  7872  genprndl  7894  genprndu  7895  genpdisj  7896  addlocprlemgt  7907  addlocpr  7909  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  mulnqprlemrl  7946  mulnqprlemru  7947  ltpopr  7968  ltexprlemloc  7980  ltexprlemrl  7983  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemladdfu  8050  suplocexprlemru  8092  axcaucvglemres  8272  cnegex  8511  mullt0  8815  eqord1  8818  mulge0  8955  divap0  9022  div2negap  9073  prodgt0  9190  ltmul12a  9198  recgt1i  9236  div4p1lem1div2  9570  nn0lt2  9736  peano5uzti  9764  btwnapz  9786  eluzp1m1  9961  eluzaddi  9964  eluzsubi  9965  uz2m1nn  10020  rphalflt  10100  xleaddadd  10305  ixxdisj  10321  iccgelb  10350  icodisj  10410  iccf1o  10423  fzsuc2  10502  fzonmapblen  10615  zsupcllemstep  10678  nninfdcex  10688  flqge0nn0  10748  flqge1nn  10749  modfzo0difsn  10852  nninfinf  10900  seqf1oglem2  10977  expubnd  11053  bernneq  11118  bernneq2  11119  nn0opthlem2d  11180  facwordi  11199  bcpasc  11225  hashnncl  11255  ccatsymb  11391  ccatass  11397  ccat1st1st  11430  fzowrddc  11440  swrdlend  11451  swrdfv2  11456  swrdspsleq  11460  pfxeq  11489  pfxsuff1eqwrdeq  11492  swrdswrdlem  11497  swrdswrd  11498  swrdpfx  11500  ccats1pfxeqrex  11508  pfxccatin12lem1  11521  swrdccatin2  11522  recvguniq  11782  sqrt0rlem  11790  resqrexlemover  11797  resqrexlemcalc3  11803  resqrexlemgt0  11807  resqrexlemoverl  11808  recvalap  11885  nnabscl  11888  negfi  12016  2zinfmin  12033  climi0  12079  climge0  12115  summodclem3  12171  fsumsplit  12198  fisumcom2  12229  fisumrev2  12237  explecnv  12296  cvgratnnlemseq  12317  fprodsplitdc  12387  fprodsplit  12388  fprodcom2fi  12417  eftlub  12481  sin02gt0  12555  dvdslelemd  12634  dvdsleabs2  12637  mulmoddvds  12654  odd2np1  12664  oexpneg  12668  mod2eq1n2dvds  12670  sqoddm1div8z  12677  rplpwr  12828  rppwr  12829  nn0seqcvgd  12843  lcmneg  12876  qredeq  12898  dvdsnprmd  12927  oddprmge3  12938  nnmaxpwlemdvds  12973  nnmaxpwlemndvds  12974  nnmaxpwlemnfac  12975  znege1  12982  qgt0numnn  13003  phibndlem  13022  hashgcdeq  13046  reumodprminv  13060  coprimeprodsq2  13065  pythagtrip  13090  pceq0  13129  dvdsprmpweqle  13144  fldivp1  13155  4sqlem9  13193  4sqlem15  13212  4sqlem16  13213  ballotfilemfrcn0  13330  ennnfonelemf1  13366  imasmnd  13818  imasgrp  13972  subginv  14042  subgmulg  14049  eqger  14085  kerf1ghm  14135  gsummptfidmsplit  14253  rngpropd  14360  rng1zrlem  14364  srgidmlem  14388  ringpropd  14449  crngpropd  14450  imasring  14477  rhmf1o  14583  subrngpropd  14632  subrg1  14647  subrgpropd  14669  rrgnz  14685  aprsym  14704  aprcotr  14705  aprlring  14708  lmodprop2d  14793  lssssg  14805  lss0cl  14814  isridlrng  14927  rspcl  14936  rspssid  14937  rnglidlmmgm  14941  psrbaglefifi  15175  psrgrp  15204  neiuni  15404  neissex  15408  tgrest  15412  tgcnp  15452  lmfpm  15486  lmcl  15488  lmss  15489  lmff  15492  psmetdmdm  15567  xmeter  15679  neibl  15734  xmettxlem  15752  tgqioo  15798  cnopnap  15854  limcimo  15908  dvidsslem  15936  sinq12gt0  16074  logrpap0  16124  pellexlem2  16247  ppiqeq0  16297  ppiqub  16310  chtqleppi  16311  mersenne  16314  lgsdilem  16368  lgsdinn0  16389  gausslemma2dlem0b  16391  gausslemma2dlem1a  16399  gausslemma2dlem5  16407  gausslemma2dlem6  16408  lgsquad3  16425  m1lgs  16426  2lgslem1a  16429  2lgslem1  16432  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2sqlem6  16461  edgupgren  16604  upgredg  16607  wlkl1loop  16821  wlk1walkdom  16822  upgriswlkdc  16823  loopclwwlkn1b  16882  eupth2lembfi  16940  dichmul0orlem6  16980  isomninnlem  17302  ismkvnnlem  17326