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  601  biadanid  614  bimsc1  965  biimp3a  1356  equsex  1739  euor  2064  euan  2094  cgsexg  2787  cgsex2g  2788  cgsex4g  2789  ceqsex  2790  sbciegft  3008  sbeqalb  3034  sseqtrid  3220  exmidn0m  4219  euotd  4272  ralxfr2d  4482  rexxfr2d  4483  nlimsucg  4583  wetriext  4594  relop  4795  resiexg  4970  iotass  5213  fnbr  5337  f1o00  5515  foelcdmi  5589  fnex  5759  foelrn  5774  acexmidlemab  5890  f1ocnv2d  6098  ofrval  6117  eloprabi  6221  1stconst  6246  2ndconst  6247  poxp  6257  smodm2  6320  smoiso  6327  nnsucuniel  6520  erth  6605  iinerm  6633  pw2f1odclem  6862  pw2f1odc  6863  phplem4dom  6890  findcard2  6917  findcard2s  6918  fimax2gtrilemstep  6928  undifdcss  6951  fipwssg  7008  supelti  7031  nlt1pig  7370  dfplpq2  7383  ltsonq  7427  archnqq  7446  nqnq0pi  7467  prarloclemn  7528  genprndl  7550  genprndu  7551  genpdisj  7552  addlocprlemgt  7563  addlocpr  7565  nqprl  7580  nqpru  7581  addnqprlemrl  7586  addnqprlemru  7587  mulnqprlemrl  7602  mulnqprlemru  7603  ltpopr  7624  ltexprlemloc  7636  ltexprlemrl  7639  cauappcvgprlemladdfu  7683  cauappcvgprlemladdfl  7684  caucvgprlemladdfu  7706  suplocexprlemru  7748  axcaucvglemres  7928  cnegex  8165  mullt0  8467  eqord1  8470  mulge0  8606  divap0  8671  div2negap  8722  prodgt0  8839  ltmul12a  8847  recgt1i  8885  div4p1lem1div2  9202  nn0lt2  9364  peano5uzti  9391  btwnapz  9413  eluzp1m1  9581  eluzaddi  9584  eluzsubi  9585  uz2m1nn  9635  rphalflt  9713  xleaddadd  9917  ixxdisj  9933  iccgelb  9962  icodisj  10022  iccf1o  10034  fzsuc2  10109  fzonmapblen  10217  flqge0nn0  10324  flqge1nn  10325  modfzo0difsn  10426  expubnd  10608  bernneq  10672  bernneq2  10673  nn0opthlem2d  10733  facwordi  10752  bcpasc  10778  hashnncl  10807  recvguniq  11036  sqrt0rlem  11044  resqrexlemover  11051  resqrexlemcalc3  11057  resqrexlemgt0  11061  resqrexlemoverl  11062  recvalap  11138  nnabscl  11141  negfi  11268  2zinfmin  11283  climi0  11329  climge0  11365  summodclem3  11420  fsumsplit  11447  fisumcom2  11478  fisumrev2  11486  explecnv  11545  cvgratnnlemseq  11566  fprodsplitdc  11636  fprodsplit  11637  fprodcom2fi  11666  eftlub  11730  sin02gt0  11803  dvdslelemd  11881  dvdsleabs2  11884  mulmoddvds  11901  odd2np1  11910  oexpneg  11914  mod2eq1n2dvds  11916  sqoddm1div8z  11923  zsupcllemstep  11978  nninfdcex  11986  rplpwr  12060  rppwr  12061  nn0seqcvgd  12073  lcmneg  12106  qredeq  12128  dvdsnprmd  12157  oddprmge3  12167  oddpwdclemdvds  12202  oddpwdclemndvds  12203  oddpwdclemodd  12204  znege1  12210  qgt0numnn  12231  phibndlem  12248  hashgcdeq  12271  reumodprminv  12285  coprimeprodsq2  12290  pythagtrip  12315  pceq0  12354  dvdsprmpweqle  12369  fldivp1  12380  4sqlem9  12418  4sqlem15  12437  4sqlem16  12438  ennnfonelemf1  12469  imasgrp  13053  subginv  13120  subgmulg  13127  eqger  13163  kerf1ghm  13213  rngpropd  13309  srgidmlem  13332  srg1zr  13341  ringpropd  13392  crngpropd  13393  imasring  13414  rhmf1o  13518  subrngpropd  13563  subrg1  13578  subrgpropd  13595  aprsym  13600  aprcotr  13601  lmodprop2d  13664  lssssg  13676  lss0cl  13685  isridlrng  13798  rspcl  13807  rspssid  13808  rnglidlmmgm  13812  neiuni  14118  neissex  14122  tgrest  14126  tgcnp  14166  lmfpm  14200  lmcl  14202  lmss  14203  lmff  14206  psmetdmdm  14281  xmeter  14393  neibl  14448  xmettxlem  14466  tgqioo  14504  cnopnap  14551  limcimo  14591  sinq12gt0  14708  logrpap0  14755  lgsdilem  14886  lgsdinn0  14907  m1lgs  14910  2sqlem6  14925  isomninnlem  15237  ismkvnnlem  15259