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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117

This theorem is used 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  4338  euotd  4395  ralxfr2d  4610  rexxfr2d  4611  nlimsucg  4713  wetriext  4724  relop  4930  resiexg  5108  iotass  5355  fnbr  5485  f1o00  5676  foelcdmi  5755  fnex  5937  foelrn  5958  riotaeqimp  6063  acexmidlemab  6079  f1ocnv2d  6294  f1o3d  6298  ofrval  6313  elabreximd  6356  eloprabi  6432  1stconst  6457  2ndconst  6458  poxp  6468  smodm2  6566  smoiso  6573  nnsucuniel  6768  erth  6853  iinerm  6881  pw2f1odclem  7134  pw2f1odc  7135  phplem4dom  7163  findcard2  7193  findcard2s  7194  fimax2gtrilemstep  7205  undifdcss  7230  tpfidceq  7237  fipwssg  7313  2omap  7318  supelti  7342  nlt1pig  7708  dfplpq2  7721  ltsonq  7765  archnqq  7784  nqnq0pi  7805  prarloclemn  7866  genprndl  7888  genprndu  7889  genpdisj  7890  addlocprlemgt  7901  addlocpr  7903  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  mulnqprlemrl  7940  mulnqprlemru  7941  ltpopr  7962  ltexprlemloc  7974  ltexprlemrl  7977  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemladdfu  8044  suplocexprlemru  8086  axcaucvglemres  8266  cnegex  8505  mullt0  8809  eqord1  8812  mulge0  8949  divap0  9016  div2negap  9067  prodgt0  9184  ltmul12a  9192  recgt1i  9230  div4p1lem1div2  9563  nn0lt2  9731  peano5uzti  9758  btwnapz  9780  eluzp1m1  9955  eluzaddi  9958  eluzsubi  9959  uz2m1nn  10014  rphalflt  10094  xleaddadd  10299  ixxdisj  10315  iccgelb  10344  icodisj  10404  iccf1o  10417  fzsuc2  10496  fzonmapblen  10609  zsupcllemstep  10672  nninfdcex  10682  flqge0nn0  10741  flqge1nn  10742  modfzo0difsn  10845  nninfinf  10893  seqf1oglem2  10970  expubnd  11046  bernneq  11111  bernneq2  11112  nn0opthlem2d  11173  facwordi  11192  bcpasc  11218  hashnncl  11248  ccatsymb  11384  ccatass  11390  ccat1st1st  11423  fzowrddc  11433  swrdlend  11444  swrdfv2  11449  swrdspsleq  11453  pfxeq  11482  pfxsuff1eqwrdeq  11485  swrdswrdlem  11490  swrdswrd  11491  swrdpfx  11493  ccats1pfxeqrex  11501  pfxccatin12lem1  11514  swrdccatin2  11515  recvguniq  11775  sqrt0rlem  11783  resqrexlemover  11790  resqrexlemcalc3  11796  resqrexlemgt0  11800  resqrexlemoverl  11801  recvalap  11878  nnabscl  11881  negfi  12009  2zinfmin  12025  climi0  12071  climge0  12107  summodclem3  12163  fsumsplit  12190  fisumcom2  12221  fisumrev2  12229  explecnv  12288  cvgratnnlemseq  12309  fprodsplitdc  12379  fprodsplit  12380  fprodcom2fi  12409  eftlub  12473  sin02gt0  12547  dvdslelemd  12626  dvdsleabs2  12629  mulmoddvds  12646  odd2np1  12656  oexpneg  12660  mod2eq1n2dvds  12662  sqoddm1div8z  12669  rplpwr  12820  rppwr  12821  nn0seqcvgd  12835  lcmneg  12868  qredeq  12890  dvdsnprmd  12919  oddprmge3  12930  nnmaxpwlemdvds  12965  nnmaxpwlemndvds  12966  nnmaxpwlemnfac  12967  znege1  12974  qgt0numnn  12995  phibndlem  13014  hashgcdeq  13038  reumodprminv  13052  coprimeprodsq2  13057  pythagtrip  13082  pceq0  13121  dvdsprmpweqle  13136  fldivp1  13147  4sqlem9  13185  4sqlem15  13204  4sqlem16  13205  ballotfilemfrcn0  13322  ennnfonelemf1  13358  imasmnd  13809  imasgrp  13963  subginv  14033  subgmulg  14040  eqger  14076  kerf1ghm  14126  rngpropd  14303  rng1zrlem  14307  srgidmlem  14331  ringpropd  14392  crngpropd  14393  imasring  14418  rhmf1o  14524  subrngpropd  14573  subrg1  14588  subrgpropd  14610  rrgnz  14626  aprsym  14645  aprcotr  14646  aprlring  14649  lmodprop2d  14734  lssssg  14746  lss0cl  14755  isridlrng  14868  rspcl  14877  rspssid  14878  rnglidlmmgm  14882  psrbagfsupp  15104  psrgrp  15125  mplsubgfilemcl  15139  neiuni  15311  neissex  15315  tgrest  15319  tgcnp  15359  lmfpm  15393  lmcl  15395  lmss  15396  lmff  15399  psmetdmdm  15474  xmeter  15586  neibl  15641  xmettxlem  15659  tgqioo  15705  cnopnap  15761  limcimo  15815  dvidsslem  15843  sinq12gt0  15981  logrpap0  16029  pellexlem2  16149  ppiqeq0  16182  ppiqub  16194  mersenne  16195  lgsdilem  16244  lgsdinn0  16265  gausslemma2dlem0b  16267  gausslemma2dlem1a  16275  gausslemma2dlem5  16283  gausslemma2dlem6  16284  lgsquad3  16301  m1lgs  16302  2lgslem1a  16305  2lgslem1  16308  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  2sqlem6  16337  edgupgren  16480  upgredg  16483  wlkl1loop  16697  wlk1walkdom  16698  upgriswlkdc  16699  loopclwwlkn1b  16758  eupth2lembfi  16816  dichmul0orlem6  16856  isomninnlem  17177  ismkvnnlem  17200