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  381  simplbda  382  pm5.1  591  bimsc1  953  biimp3a  1335  equsex  1716  euor  2040  euan  2070  cgsexg  2760  cgsex2g  2761  cgsex4g  2762  ceqsex  2763  sbciegft  2980  sbeqalb  3006  sseqtrid  3191  exmidn0m  4179  euotd  4231  ralxfr2d  4441  rexxfr2d  4442  nlimsucg  4542  wetriext  4553  relop  4753  resiexg  4928  iotass  5169  fnbr  5289  f1o00  5466  fnex  5706  foelrn  5720  acexmidlemab  5835  f1ocnv2d  6041  ofrval  6059  eloprabi  6161  1stconst  6185  2ndconst  6186  poxp  6196  smodm2  6259  smoiso  6266  nnsucuniel  6459  erth  6541  iinerm  6569  phplem4dom  6824  findcard2  6851  findcard2s  6852  fimax2gtrilemstep  6862  undifdcss  6884  fipwssg  6940  supelti  6963  nlt1pig  7278  dfplpq2  7291  ltsonq  7335  archnqq  7354  nqnq0pi  7375  prarloclemn  7436  genprndl  7458  genprndu  7459  genpdisj  7460  addlocprlemgt  7471  addlocpr  7473  nqprl  7488  nqpru  7489  addnqprlemrl  7494  addnqprlemru  7495  mulnqprlemrl  7510  mulnqprlemru  7511  ltpopr  7532  ltexprlemloc  7544  ltexprlemrl  7547  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  caucvgprlemladdfu  7614  suplocexprlemru  7656  axcaucvglemres  7836  cnegex  8072  mullt0  8374  eqord1  8377  mulge0  8513  divap0  8576  div2negap  8627  prodgt0  8743  ltmul12a  8751  recgt1i  8789  div4p1lem1div2  9106  nn0lt2  9268  peano5uzti  9295  btwnapz  9317  eluzp1m1  9485  eluzaddi  9488  eluzsubi  9489  uz2m1nn  9539  rphalflt  9615  xleaddadd  9819  ixxdisj  9835  iccgelb  9864  icodisj  9924  iccf1o  9936  fzsuc2  10010  fzonmapblen  10118  flqge0nn0  10224  flqge1nn  10225  modfzo0difsn  10326  expubnd  10508  bernneq  10571  bernneq2  10572  nn0opthlem2d  10630  facwordi  10649  bcpasc  10675  hashnncl  10705  recvguniq  10933  sqrt0rlem  10941  resqrexlemover  10948  resqrexlemcalc3  10954  resqrexlemgt0  10958  resqrexlemoverl  10959  recvalap  11035  nnabscl  11038  negfi  11165  2zinfmin  11180  climi0  11226  climge0  11262  summodclem3  11317  fsumsplit  11344  fisumcom2  11375  fisumrev2  11383  explecnv  11442  cvgratnnlemseq  11463  fprodsplitdc  11533  fprodsplit  11534  fprodcom2fi  11563  eftlub  11627  sin02gt0  11700  dvdslelemd  11777  dvdsleabs2  11780  mulmoddvds  11797  odd2np1  11806  oexpneg  11810  mod2eq1n2dvds  11812  sqoddm1div8z  11819  zsupcllemstep  11874  nninfdcex  11882  rplpwr  11956  rppwr  11957  nn0seqcvgd  11969  lcmneg  12002  qredeq  12024  dvdsnprmd  12053  oddprmge3  12063  oddpwdclemdvds  12098  oddpwdclemndvds  12099  oddpwdclemodd  12100  znege1  12106  qgt0numnn  12127  phibndlem  12144  hashgcdeq  12167  reumodprminv  12181  coprimeprodsq2  12186  pythagtrip  12211  pceq0  12249  dvdsprmpweqle  12264  fldivp1  12274  4sqlem9  12312  ennnfonelemf1  12347  neiuni  12761  neissex  12765  tgrest  12769  tgcnp  12809  lmfpm  12843  lmcl  12845  lmss  12846  lmff  12849  psmetdmdm  12924  xmeter  13036  neibl  13091  xmettxlem  13109  tgqioo  13147  cnopnap  13194  limcimo  13234  sinq12gt0  13351  logrpap0  13398  lgsdilem  13528  lgsdinn0  13549  2sqlem6  13556  isomninnlem  13869  ismkvnnlem  13891