Theorem biimpa 294

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 143	. 2 |- ( ph -> ( ps -> ch ) )
3	2	imp 123	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  simprbda  381  simplbda  382  pm5.1  596  bimsc1  958  biimp3a  1340  equsex  1721  euor  2045  euan  2075  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  ceqsex  2768  sbciegft  2985  sbeqalb  3011  sseqtrid  3197  exmidn0m  4187  euotd  4239  ralxfr2d  4449  rexxfr2d  4450  nlimsucg  4550  wetriext  4561  relop  4761  resiexg  4936  iotass  5177  fnbr  5300  f1o00  5477  fnex  5718  foelrn  5732  acexmidlemab  5847  f1ocnv2d  6053  ofrval  6071  eloprabi  6175  1stconst  6200  2ndconst  6201  poxp  6211  smodm2  6274  smoiso  6281  nnsucuniel  6474  erth  6557  iinerm  6585  phplem4dom  6840  findcard2  6867  findcard2s  6868  fimax2gtrilemstep  6878  undifdcss  6900  fipwssg  6956  supelti  6979  nlt1pig  7303  dfplpq2  7316  ltsonq  7360  archnqq  7379  nqnq0pi  7400  prarloclemn  7461  genprndl  7483  genprndu  7484  genpdisj  7485  addlocprlemgt  7496  addlocpr  7498  nqprl  7513  nqpru  7514  addnqprlemrl  7519  addnqprlemru  7520  mulnqprlemrl  7535  mulnqprlemru  7536  ltpopr  7557  ltexprlemloc  7569  ltexprlemrl  7572  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  caucvgprlemladdfu  7639  suplocexprlemru  7681  axcaucvglemres  7861  cnegex  8097  mullt0  8399  eqord1  8402  mulge0  8538  divap0  8601  div2negap  8652  prodgt0  8768  ltmul12a  8776  recgt1i  8814  div4p1lem1div2  9131  nn0lt2  9293  peano5uzti  9320  btwnapz  9342  eluzp1m1  9510  eluzaddi  9513  eluzsubi  9514  uz2m1nn  9564  rphalflt  9640  xleaddadd  9844  ixxdisj  9860  iccgelb  9889  icodisj  9949  iccf1o  9961  fzsuc2  10035  fzonmapblen  10143  flqge0nn0  10249  flqge1nn  10250  modfzo0difsn  10351  expubnd  10533  bernneq  10596  bernneq2  10597  nn0opthlem2d  10655  facwordi  10674  bcpasc  10700  hashnncl  10730  recvguniq  10959  sqrt0rlem  10967  resqrexlemover  10974  resqrexlemcalc3  10980  resqrexlemgt0  10984  resqrexlemoverl  10985  recvalap  11061  nnabscl  11064  negfi  11191  2zinfmin  11206  climi0  11252  climge0  11288  summodclem3  11343  fsumsplit  11370  fisumcom2  11401  fisumrev2  11409  explecnv  11468  cvgratnnlemseq  11489  fprodsplitdc  11559  fprodsplit  11560  fprodcom2fi  11589  eftlub  11653  sin02gt0  11726  dvdslelemd  11803  dvdsleabs2  11806  mulmoddvds  11823  odd2np1  11832  oexpneg  11836  mod2eq1n2dvds  11838  sqoddm1div8z  11845  zsupcllemstep  11900  nninfdcex  11908  rplpwr  11982  rppwr  11983  nn0seqcvgd  11995  lcmneg  12028  qredeq  12050  dvdsnprmd  12079  oddprmge3  12089  oddpwdclemdvds  12124  oddpwdclemndvds  12125  oddpwdclemodd  12126  znege1  12132  qgt0numnn  12153  phibndlem  12170  hashgcdeq  12193  reumodprminv  12207  coprimeprodsq2  12212  pythagtrip  12237  pceq0  12275  dvdsprmpweqle  12290  fldivp1  12300  4sqlem9  12338  ennnfonelemf1  12373  neiuni  12955  neissex  12959  tgrest  12963  tgcnp  13003  lmfpm  13037  lmcl  13039  lmss  13040  lmff  13043  psmetdmdm  13118  xmeter  13230  neibl  13285  xmettxlem  13303  tgqioo  13341  cnopnap  13388  limcimo  13428  sinq12gt0  13545  logrpap0  13592  lgsdilem  13722  lgsdinn0  13743  2sqlem6  13750  isomninnlem  14062  ismkvnnlem  14084