Theorem biimprd 158

Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimprd.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimprd	|- ( ph -> ( ch -> ps ) )

Proof of Theorem biimprd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2		biimprd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	imbitrrid 156	1 |- ( ph -> ( ch -> ps ) )

Syntax hints:   -> wi 4   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimtrrdi  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  673  mtbii  675  orbi2d  791  pm3.11dc  959  prlem1  975  nfimd  1596  dral1  1741  cbvalv1  1762  cbvalh  1764  ax16i  1869  speiv  1873  a16g  1875  cbvalvw  1931  cbvexvw  1932  cleqh  2293  pm13.18  2445  rspcimdv  2866  rspcimedv  2867  rspcedv  2869  moi2  2942  moi  2944  eqrd  3198  abnexg  4478  ralxfrd  4494  ralxfr2d  4496  rexxfr2d  4497  elres  4979  2elresin  5366  f1ocnv  5514  tz6.12c  5585  fvun1  5624  dffo4  5707  isores3  5859  tposfo2  6322  issmo2  6344  iordsmo  6352  smoel2  6358  fiintim  6987  ismkvnex  7216  prarloclemarch  7480  genprndl  7583  genprndu  7584  ltpopr  7657  ltsopr  7658  recexprlem1ssl  7695  recexprlem1ssu  7696  aptiprlemu  7702  lttrsr  7824  aptap  8671  rerecapb  8864  nnmulcl  9005  nnnegz  9323  eluzdc  9678  negm  9683  iccid  9994  icoshft  10059  fzen  10112  elfz2nn0  10181  elfzom1p1elfzo  10284  flqeqceilz  10392  zmodidfzoimp  10428  caucvgre  11128  qdenre  11349  dvdsval2  11936  negdvdsb  11953  muldvds2  11963  dvdsabseq  11992  bezoutlemaz  12143  bezoutlembz  12144  rplpwr  12167  alginv  12188  algfx  12193  coprmgcdb  12229  divgcdcoprm0  12242  prmgt1  12273  oddprmgt2  12275  rpexp1i  12295  2sqpwodd  12317  qnumdencl  12328  phiprmpw  12363  prmdiveq  12377  prm23lt5  12404  pcmpt  12484  infpnlem1  12500  oddennn  12552  nninfdclemf1  12612  imasaddfnlemg  12900  aprcotr  13784  cnpnei  14398  bl2in  14582  addcncntoplem  14740  rescncf  14760  limcresi  14845  cnplimcim  14846  efltlemlt  14950  ioocosf1o  15030  2lgslem1a1  15243  uzdcinzz  15360  bj-charfunbi  15373  bj-omssind  15497  bj-bdfindes  15511  bj-nntrans  15513  bj-nnelirr  15515  bj-omtrans  15518  setindis  15529  bdsetindis  15531  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535  bj-findis  15541  bj-findes  15543