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  5621  foelcdmi  5699  fnex  5877  foelrn  5896  riotaeqimp  5999  acexmidlemab  6015  f1ocnv2d  6230  ofrval  6249  eloprabi  6364  1stconst  6389  2ndconst  6390  poxp  6400  smodm2  6464  smoiso  6471  nnsucuniel  6666  erth  6751  iinerm  6779  pw2f1odclem  7023  pw2f1odc  7024  phplem4dom  7051  findcard2  7081  findcard2s  7082  fimax2gtrilemstep  7093  undifdcss  7118  tpfidceq  7125  fipwssg  7181  supelti  7204  nlt1pig  7564  dfplpq2  7577  ltsonq  7621  archnqq  7640  nqnq0pi  7661  prarloclemn  7722  genprndl  7744  genprndu  7745  genpdisj  7746  addlocprlemgt  7757  addlocpr  7759  nqprl  7774  nqpru  7775  addnqprlemrl  7780  addnqprlemru  7781  mulnqprlemrl  7796  mulnqprlemru  7797  ltpopr  7818  ltexprlemloc  7830  ltexprlemrl  7833  cauappcvgprlemladdfu  7877  cauappcvgprlemladdfl  7878  caucvgprlemladdfu  7900  suplocexprlemru  7942  axcaucvglemres  8122  cnegex  8360  mullt0  8663  eqord1  8666  mulge0  8802  divap0  8867  div2negap  8918  prodgt0  9035  ltmul12a  9043  recgt1i  9081  div4p1lem1div2  9401  nn0lt2  9564  peano5uzti  9591  btwnapz  9613  eluzp1m1  9783  eluzaddi  9786  eluzsubi  9787  uz2m1nn  9842  rphalflt  9921  xleaddadd  10125  ixxdisj  10141  iccgelb  10170  icodisj  10230  iccf1o  10242  fzsuc2  10317  fzonmapblen  10430  zsupcllemstep  10493  nninfdcex  10501  flqge0nn0  10557  flqge1nn  10558  modfzo0difsn  10661  nninfinf  10709  seqf1oglem2  10786  expubnd  10862  bernneq  10926  bernneq2  10927  nn0opthlem2d  10987  facwordi  11006  bcpasc  11032  hashnncl  11061  ccatsymb  11186  ccatass  11192  ccat1st1st  11225  fzowrddc  11235  swrdlend  11246  swrdfv2  11251  swrdspsleq  11255  pfxeq  11284  pfxsuff1eqwrdeq  11287  swrdswrdlem  11292  swrdswrd  11293  swrdpfx  11295  ccats1pfxeqrex  11303  pfxccatin12lem1  11316  swrdccatin2  11317  recvguniq  11576  sqrt0rlem  11584  resqrexlemover  11591  resqrexlemcalc3  11597  resqrexlemgt0  11601  resqrexlemoverl  11602  recvalap  11678  nnabscl  11681  negfi  11809  2zinfmin  11824  climi0  11870  climge0  11906  summodclem3  11962  fsumsplit  11989  fisumcom2  12020  fisumrev2  12028  explecnv  12087  cvgratnnlemseq  12108  fprodsplitdc  12178  fprodsplit  12179  fprodcom2fi  12208  eftlub  12272  sin02gt0  12346  dvdslelemd  12425  dvdsleabs2  12428  mulmoddvds  12445  odd2np1  12455  oexpneg  12459  mod2eq1n2dvds  12461  sqoddm1div8z  12468  rplpwr  12619  rppwr  12620  nn0seqcvgd  12634  lcmneg  12667  qredeq  12689  dvdsnprmd  12718  oddprmge3  12728  oddpwdclemdvds  12763  oddpwdclemndvds  12764  oddpwdclemodd  12765  znege1  12771  qgt0numnn  12792  phibndlem  12809  hashgcdeq  12833  reumodprminv  12847  coprimeprodsq2  12852  pythagtrip  12877  pceq0  12916  dvdsprmpweqle  12931  fldivp1  12942  4sqlem9  12980  4sqlem15  12999  4sqlem16  13000  ennnfonelemf1  13060  imasmnd  13557  imasgrp  13719  subginv  13789  subgmulg  13796  eqger  13832  kerf1ghm  13882  rngpropd  13990  srgidmlem  14013  srg1zr  14022  ringpropd  14073  crngpropd  14074  imasring  14099  rhmf1o  14204  subrngpropd  14252  subrg1  14267  subrgpropd  14289  rrgnz  14304  aprsym  14320  aprcotr  14321  lmodprop2d  14384  lssssg  14396  lss0cl  14405  isridlrng  14518  rspcl  14527  rspssid  14528  rnglidlmmgm  14532  psrgrp  14726  mplsubgfilemcl  14740  neiuni  14912  neissex  14916  tgrest  14920  tgcnp  14960  lmfpm  14994  lmcl  14996  lmss  14997  lmff  15000  psmetdmdm  15075  xmeter  15187  neibl  15242  xmettxlem  15260  tgqioo  15306  cnopnap  15362  limcimo  15416  dvidsslem  15444  sinq12gt0  15581  logrpap0  15628  mersenne  15748  lgsdilem  15783  lgsdinn0  15804  gausslemma2dlem0b  15806  gausslemma2dlem1a  15814  gausslemma2dlem5  15822  gausslemma2dlem6  15823  lgsquad3  15840  m1lgs  15841  2lgslem1a  15844  2lgslem1  15847  2lgslem3a1  15853  2lgslem3b1  15854  2lgslem3c1  15855  2lgslem3d1  15856  2sqlem6  15876  edgupgren  16019  upgredg  16022  wlkl1loop  16236  wlk1walkdom  16237  upgriswlkdc  16238  loopclwwlkn1b  16297  eupth2lembfi  16355  2omap  16653  isomninnlem  16693  ismkvnnlem  16716