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  4340  euotd  4397  ralxfr2d  4612  rexxfr2d  4613  nlimsucg  4715  wetriext  4726  relop  4932  resiexg  5111  iotass  5358  fnbr  5488  f1o00  5679  foelcdmi  5758  fnex  5940  foelrn  5961  riotaeqimp  6066  acexmidlemab  6082  f1ocnv2d  6297  f1o3d  6301  ofrval  6317  elabreximd  6360  eloprabi  6436  1stconst  6461  2ndconst  6462  poxp  6472  smodm2  6570  smoiso  6577  nnsucuniel  6772  erth  6857  iinerm  6885  pw2f1odclem  7138  pw2f1odc  7139  phplem4dom  7167  findcard2  7197  findcard2s  7198  fimax2gtrilemstep  7209  undifdcss  7234  tpfidceq  7241  fipwssg  7318  2omap  7324  supelti  7348  nlt1pig  7714  dfplpq2  7727  ltsonq  7771  archnqq  7790  nqnq0pi  7811  prarloclemn  7872  genprndl  7894  genprndu  7895  genpdisj  7896  addlocprlemgt  7907  addlocpr  7909  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  mulnqprlemrl  7946  mulnqprlemru  7947  ltpopr  7968  ltexprlemloc  7980  ltexprlemrl  7983  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemladdfu  8050  suplocexprlemru  8092  axcaucvglemres  8272  cnegex  8511  mullt0  8815  eqord1  8818  mulge0  8955  divap0  9022  div2negap  9073  prodgt0  9190  ltmul12a  9198  recgt1i  9236  div4p1lem1div2  9570  nn0lt2  9738  peano5uzti  9765  btwnapz  9787  eluzp1m1  9962  eluzaddi  9965  eluzsubi  9966  uz2m1nn  10021  rphalflt  10101  xleaddadd  10306  ixxdisj  10322  iccgelb  10351  icodisj  10411  iccf1o  10424  fzsuc2  10503  fzonmapblen  10616  zsupcllemstep  10679  nninfdcex  10689  flqge0nn0  10749  flqge1nn  10750  modfzo0difsn  10853  nninfinf  10901  seqf1oglem2  10978  expubnd  11054  bernneq  11119  bernneq2  11120  nn0opthlem2d  11181  facwordi  11200  bcpasc  11226  hashnncl  11256  ccatsymb  11392  ccatass  11398  ccat1st1st  11431  fzowrddc  11441  swrdlend  11452  swrdfv2  11457  swrdspsleq  11461  pfxeq  11490  pfxsuff1eqwrdeq  11493  swrdswrdlem  11498  swrdswrd  11499  swrdpfx  11501  ccats1pfxeqrex  11509  pfxccatin12lem1  11522  swrdccatin2  11523  recvguniq  11783  sqrt0rlem  11791  resqrexlemover  11798  resqrexlemcalc3  11804  resqrexlemgt0  11808  resqrexlemoverl  11809  recvalap  11886  nnabscl  11889  negfi  12017  2zinfmin  12034  climi0  12080  climge0  12116  summodclem3  12172  fsumsplit  12199  fisumcom2  12230  fisumrev2  12238  explecnv  12297  cvgratnnlemseq  12318  fprodsplitdc  12388  fprodsplit  12389  fprodcom2fi  12418  eftlub  12482  sin02gt0  12556  dvdslelemd  12635  dvdsleabs2  12638  mulmoddvds  12655  odd2np1  12665  oexpneg  12669  mod2eq1n2dvds  12671  sqoddm1div8z  12678  rplpwr  12829  rppwr  12830  nn0seqcvgd  12844  lcmneg  12877  qredeq  12899  dvdsnprmd  12928  oddprmge3  12939  nnmaxpwlemdvds  12974  nnmaxpwlemndvds  12975  nnmaxpwlemnfac  12976  znege1  12983  qgt0numnn  13004  phibndlem  13023  hashgcdeq  13047  reumodprminv  13061  coprimeprodsq2  13066  pythagtrip  13091  pceq0  13130  dvdsprmpweqle  13145  fldivp1  13156  4sqlem9  13194  4sqlem15  13213  4sqlem16  13214  ballotfilemfrcn0  13331  ennnfonelemf1  13367  imasmnd  13819  imasgrp  13973  subginv  14043  subgmulg  14050  eqger  14086  kerf1ghm  14136  gsummptfidmsplit  14254  rngpropd  14361  rng1zrlem  14365  srgidmlem  14389  ringpropd  14450  crngpropd  14451  imasring  14478  rhmf1o  14584  subrngpropd  14633  subrg1  14648  subrgpropd  14670  rrgnz  14686  aprsym  14705  aprcotr  14706  aprlring  14709  lmodprop2d  14794  lssssg  14806  lss0cl  14815  isridlrng  14928  rspcl  14937  rspssid  14938  rnglidlmmgm  14942  psrbagfsupp  15164  psrbaglefifi  15172  psrgrp  15195  mplsubgfilemcl  15215  neiuni  15387  neissex  15391  tgrest  15395  tgcnp  15435  lmfpm  15469  lmcl  15471  lmss  15472  lmff  15475  psmetdmdm  15550  xmeter  15662  neibl  15717  xmettxlem  15735  tgqioo  15781  cnopnap  15837  limcimo  15891  dvidsslem  15919  sinq12gt0  16057  logrpap0  16107  pellexlem2  16230  ppiqeq0  16280  ppiqub  16293  chtqleppi  16294  mersenne  16297  lgsdilem  16351  lgsdinn0  16372  gausslemma2dlem0b  16374  gausslemma2dlem1a  16382  gausslemma2dlem5  16390  gausslemma2dlem6  16391  lgsquad3  16408  m1lgs  16409  2lgslem1a  16412  2lgslem1  16415  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  2sqlem6  16444  edgupgren  16587  upgredg  16590  wlkl1loop  16804  wlk1walkdom  16805  upgriswlkdc  16806  loopclwwlkn1b  16865  eupth2lembfi  16923  dichmul0orlem6  16963  isomninnlem  17285  ismkvnnlem  17309