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  605  biadanid  618  bimsc1  972  biimp3a  1382  equsex  1776  euor  2106  euan  2137  cgsexg  2848  cgsex2g  2849  cgsex4g  2850  ceqsex  2851  sbciegft  3072  sbeqalb  3098  sseqtrid  3287  exmidn0m  4306  euotd  4362  ralxfr2d  4576  rexxfr2d  4577  nlimsucg  4679  wetriext  4690  relop  4896  resiexg  5074  iotass  5321  fnbr  5451  f1o00  5642  foelcdmi  5720  fnex  5897  foelrn  5916  riotaeqimp  6019  acexmidlemab  6035  f1ocnv2d  6250  ofrval  6268  eloprabi  6383  1stconst  6408  2ndconst  6409  poxp  6419  smodm2  6517  smoiso  6524  nnsucuniel  6719  erth  6804  iinerm  6832  pw2f1odclem  7078  pw2f1odc  7079  phplem4dom  7107  findcard2  7137  findcard2s  7138  fimax2gtrilemstep  7149  undifdcss  7174  tpfidceq  7181  fipwssg  7257  2omap  7260  supelti  7284  nlt1pig  7644  dfplpq2  7657  ltsonq  7701  archnqq  7720  nqnq0pi  7741  prarloclemn  7802  genprndl  7824  genprndu  7825  genpdisj  7826  addlocprlemgt  7837  addlocpr  7839  nqprl  7854  nqpru  7855  addnqprlemrl  7860  addnqprlemru  7861  mulnqprlemrl  7876  mulnqprlemru  7877  ltpopr  7898  ltexprlemloc  7910  ltexprlemrl  7913  cauappcvgprlemladdfu  7957  cauappcvgprlemladdfl  7958  caucvgprlemladdfu  7980  suplocexprlemru  8022  axcaucvglemres  8202  cnegex  8439  mullt0  8742  eqord1  8745  mulge0  8881  divap0  8946  div2negap  8997  prodgt0  9114  ltmul12a  9122  recgt1i  9160  div4p1lem1div2  9480  nn0lt2  9645  peano5uzti  9672  btwnapz  9694  eluzp1m1  9864  eluzaddi  9867  eluzsubi  9868  uz2m1nn  9923  rphalflt  10002  xleaddadd  10206  ixxdisj  10222  iccgelb  10251  icodisj  10311  iccf1o  10324  fzsuc2  10399  fzonmapblen  10512  zsupcllemstep  10575  nninfdcex  10583  flqge0nn0  10639  flqge1nn  10640  modfzo0difsn  10743  nninfinf  10791  seqf1oglem2  10868  expubnd  10944  bernneq  11008  bernneq2  11009  nn0opthlem2d  11069  facwordi  11088  bcpasc  11114  hashnncl  11143  ccatsymb  11268  ccatass  11274  ccat1st1st  11307  fzowrddc  11317  swrdlend  11328  swrdfv2  11333  swrdspsleq  11337  pfxeq  11366  pfxsuff1eqwrdeq  11369  swrdswrdlem  11374  swrdswrd  11375  swrdpfx  11377  ccats1pfxeqrex  11385  pfxccatin12lem1  11398  swrdccatin2  11399  recvguniq  11658  sqrt0rlem  11666  resqrexlemover  11673  resqrexlemcalc3  11679  resqrexlemgt0  11683  resqrexlemoverl  11684  recvalap  11760  nnabscl  11763  negfi  11891  2zinfmin  11906  climi0  11952  climge0  11988  summodclem3  12044  fsumsplit  12071  fisumcom2  12102  fisumrev2  12110  explecnv  12169  cvgratnnlemseq  12190  fprodsplitdc  12260  fprodsplit  12261  fprodcom2fi  12290  eftlub  12354  sin02gt0  12428  dvdslelemd  12507  dvdsleabs2  12510  mulmoddvds  12527  odd2np1  12537  oexpneg  12541  mod2eq1n2dvds  12543  sqoddm1div8z  12550  rplpwr  12701  rppwr  12702  nn0seqcvgd  12716  lcmneg  12749  qredeq  12771  dvdsnprmd  12800  oddprmge3  12810  oddpwdclemdvds  12845  oddpwdclemndvds  12846  oddpwdclemodd  12847  znege1  12853  qgt0numnn  12874  phibndlem  12891  hashgcdeq  12915  reumodprminv  12929  coprimeprodsq2  12934  pythagtrip  12959  pceq0  12998  dvdsprmpweqle  13013  fldivp1  13024  4sqlem9  13062  4sqlem15  13081  4sqlem16  13082  ennnfonelemf1  13143  imasmnd  13640  imasgrp  13802  subginv  13872  subgmulg  13879  eqger  13915  kerf1ghm  13965  rngpropd  14073  srgidmlem  14096  srg1zr  14105  ringpropd  14156  crngpropd  14157  imasring  14182  rhmf1o  14287  subrngpropd  14335  subrg1  14350  subrgpropd  14372  rrgnz  14388  aprsym  14404  aprcotr  14405  lmodprop2d  14468  lssssg  14480  lss0cl  14489  isridlrng  14602  rspcl  14611  rspssid  14612  rnglidlmmgm  14616  psrgrp  14810  mplsubgfilemcl  14824  neiuni  14996  neissex  15000  tgrest  15004  tgcnp  15044  lmfpm  15078  lmcl  15080  lmss  15081  lmff  15084  psmetdmdm  15159  xmeter  15271  neibl  15326  xmettxlem  15344  tgqioo  15390  cnopnap  15446  limcimo  15500  dvidsslem  15528  sinq12gt0  15665  logrpap0  15712  pellexlem2  15816  mersenne  15835  lgsdilem  15870  lgsdinn0  15891  gausslemma2dlem0b  15893  gausslemma2dlem1a  15901  gausslemma2dlem5  15909  gausslemma2dlem6  15910  lgsquad3  15927  m1lgs  15928  2lgslem1a  15931  2lgslem1  15934  2lgslem3a1  15940  2lgslem3b1  15941  2lgslem3c1  15942  2lgslem3d1  15943  2sqlem6  15963  edgupgren  16106  upgredg  16109  wlkl1loop  16323  wlk1walkdom  16324  upgriswlkdc  16325  loopclwwlkn1b  16384  eupth2lembfi  16442  isomninnlem  16784  ismkvnnlem  16807