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  971  biimp3a  1381  equsex  1776  euor  2105  euan  2136  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  ceqsex  2841  sbciegft  3062  sbeqalb  3088  sseqtrid  3277  exmidn0m  4291  euotd  4347  ralxfr2d  4561  rexxfr2d  4562  nlimsucg  4664  wetriext  4675  relop  4880  resiexg  5058  iotass  5304  fnbr  5434  f1o00  5620  foelcdmi  5698  fnex  5876  foelrn  5893  riotaeqimp  5996  acexmidlemab  6012  f1ocnv2d  6227  ofrval  6246  eloprabi  6361  1stconst  6386  2ndconst  6387  poxp  6397  smodm2  6461  smoiso  6468  nnsucuniel  6663  erth  6748  iinerm  6776  pw2f1odclem  7020  pw2f1odc  7021  phplem4dom  7048  findcard2  7078  findcard2s  7079  fimax2gtrilemstep  7090  undifdcss  7115  tpfidceq  7122  fipwssg  7178  supelti  7201  nlt1pig  7561  dfplpq2  7574  ltsonq  7618  archnqq  7637  nqnq0pi  7658  prarloclemn  7719  genprndl  7741  genprndu  7742  genpdisj  7743  addlocprlemgt  7754  addlocpr  7756  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  mulnqprlemrl  7793  mulnqprlemru  7794  ltpopr  7815  ltexprlemloc  7827  ltexprlemrl  7830  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemladdfu  7897  suplocexprlemru  7939  axcaucvglemres  8119  cnegex  8357  mullt0  8660  eqord1  8663  mulge0  8799  divap0  8864  div2negap  8915  prodgt0  9032  ltmul12a  9040  recgt1i  9078  div4p1lem1div2  9398  nn0lt2  9561  peano5uzti  9588  btwnapz  9610  eluzp1m1  9780  eluzaddi  9783  eluzsubi  9784  uz2m1nn  9839  rphalflt  9918  xleaddadd  10122  ixxdisj  10138  iccgelb  10167  icodisj  10227  iccf1o  10239  fzsuc2  10314  fzonmapblen  10426  zsupcllemstep  10489  nninfdcex  10497  flqge0nn0  10553  flqge1nn  10554  modfzo0difsn  10657  nninfinf  10705  seqf1oglem2  10782  expubnd  10858  bernneq  10922  bernneq2  10923  nn0opthlem2d  10983  facwordi  11002  bcpasc  11028  hashnncl  11057  ccatsymb  11179  ccatass  11185  ccat1st1st  11218  fzowrddc  11228  swrdlend  11239  swrdfv2  11244  swrdspsleq  11248  pfxeq  11277  pfxsuff1eqwrdeq  11280  swrdswrdlem  11285  swrdswrd  11286  swrdpfx  11288  ccats1pfxeqrex  11296  pfxccatin12lem1  11309  swrdccatin2  11310  recvguniq  11556  sqrt0rlem  11564  resqrexlemover  11571  resqrexlemcalc3  11577  resqrexlemgt0  11581  resqrexlemoverl  11582  recvalap  11658  nnabscl  11661  negfi  11789  2zinfmin  11804  climi0  11850  climge0  11886  summodclem3  11942  fsumsplit  11969  fisumcom2  12000  fisumrev2  12008  explecnv  12067  cvgratnnlemseq  12088  fprodsplitdc  12158  fprodsplit  12159  fprodcom2fi  12188  eftlub  12252  sin02gt0  12326  dvdslelemd  12405  dvdsleabs2  12408  mulmoddvds  12425  odd2np1  12435  oexpneg  12439  mod2eq1n2dvds  12441  sqoddm1div8z  12448  rplpwr  12599  rppwr  12600  nn0seqcvgd  12614  lcmneg  12647  qredeq  12669  dvdsnprmd  12698  oddprmge3  12708  oddpwdclemdvds  12743  oddpwdclemndvds  12744  oddpwdclemodd  12745  znege1  12751  qgt0numnn  12772  phibndlem  12789  hashgcdeq  12813  reumodprminv  12827  coprimeprodsq2  12832  pythagtrip  12857  pceq0  12896  dvdsprmpweqle  12911  fldivp1  12922  4sqlem9  12960  4sqlem15  12979  4sqlem16  12980  ennnfonelemf1  13040  imasmnd  13537  imasgrp  13699  subginv  13769  subgmulg  13776  eqger  13812  kerf1ghm  13862  rngpropd  13970  srgidmlem  13993  srg1zr  14002  ringpropd  14053  crngpropd  14054  imasring  14079  rhmf1o  14184  subrngpropd  14232  subrg1  14247  subrgpropd  14269  rrgnz  14284  aprsym  14300  aprcotr  14301  lmodprop2d  14364  lssssg  14376  lss0cl  14385  isridlrng  14498  rspcl  14507  rspssid  14508  rnglidlmmgm  14512  psrgrp  14701  mplsubgfilemcl  14715  neiuni  14887  neissex  14891  tgrest  14895  tgcnp  14935  lmfpm  14969  lmcl  14971  lmss  14972  lmff  14975  psmetdmdm  15050  xmeter  15162  neibl  15217  xmettxlem  15235  tgqioo  15281  cnopnap  15337  limcimo  15391  dvidsslem  15419  sinq12gt0  15556  logrpap0  15603  mersenne  15723  lgsdilem  15758  lgsdinn0  15779  gausslemma2dlem0b  15781  gausslemma2dlem1a  15789  gausslemma2dlem5  15797  gausslemma2dlem6  15798  lgsquad3  15815  m1lgs  15816  2lgslem1a  15819  2lgslem1  15822  2lgslem3a1  15828  2lgslem3b1  15829  2lgslem3c1  15830  2lgslem3d1  15831  2sqlem6  15851  edgupgren  15994  upgredg  15997  wlkl1loop  16211  wlk1walkdom  16212  upgriswlkdc  16213  loopclwwlkn1b  16272  2omap  16597  isomninnlem  16637  ismkvnnlem  16659