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 )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced 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  4336  euotd  4393  ralxfr2d  4608  rexxfr2d  4609  nlimsucg  4711  wetriext  4722  relop  4928  resiexg  5106  iotass  5353  fnbr  5483  f1o00  5674  foelcdmi  5752  fnex  5931  foelrn  5951  riotaeqimp  6056  acexmidlemab  6072  f1ocnv2d  6287  f1o3d  6291  ofrval  6306  elabreximd  6349  eloprabi  6425  1stconst  6450  2ndconst  6451  poxp  6461  smodm2  6559  smoiso  6566  nnsucuniel  6761  erth  6846  iinerm  6874  pw2f1odclem  7127  pw2f1odc  7128  phplem4dom  7156  findcard2  7186  findcard2s  7187  fimax2gtrilemstep  7198  undifdcss  7223  tpfidceq  7230  fipwssg  7306  2omap  7311  supelti  7335  nlt1pig  7701  dfplpq2  7714  ltsonq  7758  archnqq  7777  nqnq0pi  7798  prarloclemn  7859  genprndl  7881  genprndu  7882  genpdisj  7883  addlocprlemgt  7894  addlocpr  7896  nqprl  7911  nqpru  7912  addnqprlemrl  7917  addnqprlemru  7918  mulnqprlemrl  7933  mulnqprlemru  7934  ltpopr  7955  ltexprlemloc  7967  ltexprlemrl  7970  cauappcvgprlemladdfu  8014  cauappcvgprlemladdfl  8015  caucvgprlemladdfu  8037  suplocexprlemru  8079  axcaucvglemres  8259  cnegex  8497  mullt0  8801  eqord1  8804  mulge0  8940  divap0  9007  div2negap  9058  prodgt0  9175  ltmul12a  9183  recgt1i  9221  div4p1lem1div2  9541  nn0lt2  9709  peano5uzti  9736  btwnapz  9758  eluzp1m1  9928  eluzaddi  9931  eluzsubi  9932  uz2m1nn  9987  rphalflt  10066  xleaddadd  10271  ixxdisj  10287  iccgelb  10316  icodisj  10376  iccf1o  10389  fzsuc2  10467  fzonmapblen  10580  zsupcllemstep  10643  nninfdcex  10653  flqge0nn0  10709  flqge1nn  10710  modfzo0difsn  10813  nninfinf  10861  seqf1oglem2  10938  expubnd  11014  bernneq  11079  bernneq2  11080  nn0opthlem2d  11140  facwordi  11159  bcpasc  11185  hashnncl  11215  ccatsymb  11351  ccatass  11357  ccat1st1st  11390  fzowrddc  11400  swrdlend  11411  swrdfv2  11416  swrdspsleq  11420  pfxeq  11449  pfxsuff1eqwrdeq  11452  swrdswrdlem  11457  swrdswrd  11458  swrdpfx  11460  ccats1pfxeqrex  11468  pfxccatin12lem1  11481  swrdccatin2  11482  recvguniq  11742  sqrt0rlem  11750  resqrexlemover  11757  resqrexlemcalc3  11763  resqrexlemgt0  11767  resqrexlemoverl  11768  recvalap  11844  nnabscl  11847  negfi  11975  2zinfmin  11990  climi0  12036  climge0  12072  summodclem3  12128  fsumsplit  12155  fisumcom2  12186  fisumrev2  12194  explecnv  12253  cvgratnnlemseq  12274  fprodsplitdc  12344  fprodsplit  12345  fprodcom2fi  12374  eftlub  12438  sin02gt0  12512  dvdslelemd  12591  dvdsleabs2  12594  mulmoddvds  12611  odd2np1  12621  oexpneg  12625  mod2eq1n2dvds  12627  sqoddm1div8z  12634  rplpwr  12785  rppwr  12786  nn0seqcvgd  12800  lcmneg  12833  qredeq  12855  dvdsnprmd  12884  oddprmge3  12894  oddpwdclemdvds  12929  oddpwdclemndvds  12930  oddpwdclemodd  12931  znege1  12937  qgt0numnn  12958  phibndlem  12975  hashgcdeq  12999  reumodprminv  13013  coprimeprodsq2  13018  pythagtrip  13043  pceq0  13082  dvdsprmpweqle  13097  fldivp1  13108  4sqlem9  13146  4sqlem15  13165  4sqlem16  13166  ballotfilemfrcn0  13254  ennnfonelemf1  13290  imasmnd  13740  imasgrp  13894  subginv  13964  subgmulg  13971  eqger  14007  kerf1ghm  14057  rngpropd  14232  rng1zrlem  14236  srgidmlem  14259  ringpropd  14319  crngpropd  14320  imasring  14345  rhmf1o  14451  subrngpropd  14500  subrg1  14515  subrgpropd  14537  rrgnz  14553  aprsym  14572  aprcotr  14573  aprlring  14576  lmodprop2d  14660  lssssg  14672  lss0cl  14681  isridlrng  14794  rspcl  14803  rspssid  14804  rnglidlmmgm  14808  psrbagfsupp  14981  psrgrp  15002  mplsubgfilemcl  15016  neiuni  15188  neissex  15192  tgrest  15196  tgcnp  15236  lmfpm  15270  lmcl  15272  lmss  15273  lmff  15276  psmetdmdm  15351  xmeter  15463  neibl  15518  xmettxlem  15536  tgqioo  15582  cnopnap  15638  limcimo  15692  dvidsslem  15720  sinq12gt0  15857  logrpap0  15904  pellexlem2  16009  mersenne  16028  lgsdilem  16063  lgsdinn0  16084  gausslemma2dlem0b  16086  gausslemma2dlem1a  16094  gausslemma2dlem5  16102  gausslemma2dlem6  16103  lgsquad3  16120  m1lgs  16121  2lgslem1a  16124  2lgslem1  16127  2lgslem3a1  16133  2lgslem3b1  16134  2lgslem3c1  16135  2lgslem3d1  16136  2sqlem6  16156  edgupgren  16299  upgredg  16302  wlkl1loop  16516  wlk1walkdom  16517  upgriswlkdc  16518  loopclwwlkn1b  16577  eupth2lembfi  16635  dichmul0orlem6  16675  isomninnlem  16987  ismkvnnlem  17010