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  8504  mullt0  8808  eqord1  8811  mulge0  8947  divap0  9014  div2negap  9065  prodgt0  9182  ltmul12a  9190  recgt1i  9228  div4p1lem1div2  9559  nn0lt2  9727  peano5uzti  9754  btwnapz  9776  eluzp1m1  9946  eluzaddi  9949  eluzsubi  9950  uz2m1nn  10005  rphalflt  10084  xleaddadd  10289  ixxdisj  10305  iccgelb  10334  icodisj  10394  iccf1o  10407  fzsuc2  10486  fzonmapblen  10599  zsupcllemstep  10662  nninfdcex  10672  flqge0nn0  10728  flqge1nn  10729  modfzo0difsn  10832  nninfinf  10880  seqf1oglem2  10957  expubnd  11033  bernneq  11098  bernneq2  11099  nn0opthlem2d  11159  facwordi  11178  bcpasc  11204  hashnncl  11234  ccatsymb  11370  ccatass  11376  ccat1st1st  11409  fzowrddc  11419  swrdlend  11430  swrdfv2  11435  swrdspsleq  11439  pfxeq  11468  pfxsuff1eqwrdeq  11471  swrdswrdlem  11476  swrdswrd  11477  swrdpfx  11479  ccats1pfxeqrex  11487  pfxccatin12lem1  11500  swrdccatin2  11501  recvguniq  11761  sqrt0rlem  11769  resqrexlemover  11776  resqrexlemcalc3  11782  resqrexlemgt0  11786  resqrexlemoverl  11787  recvalap  11863  nnabscl  11866  negfi  11994  2zinfmin  12009  climi0  12055  climge0  12091  summodclem3  12147  fsumsplit  12174  fisumcom2  12205  fisumrev2  12213  explecnv  12272  cvgratnnlemseq  12293  fprodsplitdc  12363  fprodsplit  12364  fprodcom2fi  12393  eftlub  12457  sin02gt0  12531  dvdslelemd  12610  dvdsleabs2  12613  mulmoddvds  12630  odd2np1  12640  oexpneg  12644  mod2eq1n2dvds  12646  sqoddm1div8z  12653  rplpwr  12804  rppwr  12805  nn0seqcvgd  12819  lcmneg  12852  qredeq  12874  dvdsnprmd  12903  oddprmge3  12913  oddpwdclemdvds  12948  oddpwdclemndvds  12949  oddpwdclemodd  12950  znege1  12956  qgt0numnn  12977  phibndlem  12994  hashgcdeq  13018  reumodprminv  13032  coprimeprodsq2  13037  pythagtrip  13062  pceq0  13101  dvdsprmpweqle  13116  fldivp1  13127  4sqlem9  13165  4sqlem15  13184  4sqlem16  13185  ballotfilemfrcn0  13273  ennnfonelemf1  13309  imasmnd  13760  imasgrp  13914  subginv  13984  subgmulg  13991  eqger  14027  kerf1ghm  14077  rngpropd  14254  rng1zrlem  14258  srgidmlem  14282  ringpropd  14343  crngpropd  14344  imasring  14369  rhmf1o  14475  subrngpropd  14524  subrg1  14539  subrgpropd  14561  rrgnz  14577  aprsym  14596  aprcotr  14597  aprlring  14600  lmodprop2d  14685  lssssg  14697  lss0cl  14706  isridlrng  14819  rspcl  14828  rspssid  14829  rnglidlmmgm  14833  psrbagfsupp  15055  psrgrp  15076  mplsubgfilemcl  15090  neiuni  15262  neissex  15266  tgrest  15270  tgcnp  15310  lmfpm  15344  lmcl  15346  lmss  15347  lmff  15350  psmetdmdm  15425  xmeter  15537  neibl  15592  xmettxlem  15610  tgqioo  15656  cnopnap  15712  limcimo  15766  dvidsslem  15794  sinq12gt0  15931  logrpap0  15978  pellexlem2  16092  mersenne  16111  lgsdilem  16146  lgsdinn0  16167  gausslemma2dlem0b  16169  gausslemma2dlem1a  16177  gausslemma2dlem5  16185  gausslemma2dlem6  16186  lgsquad3  16203  m1lgs  16204  2lgslem1a  16207  2lgslem1  16210  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  2sqlem6  16239  edgupgren  16382  upgredg  16385  wlkl1loop  16599  wlk1walkdom  16600  upgriswlkdc  16601  loopclwwlkn1b  16660  eupth2lembfi  16718  dichmul0orlem6  16758  isomninnlem  17079  ismkvnnlem  17102