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  2865  rspcimedv  2866  rspcedv  2868  moi2  2941  moi  2943  eqrd  3197  abnexg  4477  ralxfrd  4493  ralxfr2d  4495  rexxfr2d  4496  elres  4978  2elresin  5365  f1ocnv  5513  tz6.12c  5584  fvun1  5623  dffo4  5706  isores3  5858  tposfo2  6320  issmo2  6342  iordsmo  6350  smoel2  6356  fiintim  6985  ismkvnex  7214  prarloclemarch  7478  genprndl  7581  genprndu  7582  ltpopr  7655  ltsopr  7656  recexprlem1ssl  7693  recexprlem1ssu  7694  aptiprlemu  7700  lttrsr  7822  aptap  8669  rerecapb  8862  nnmulcl  9003  nnnegz  9320  eluzdc  9675  negm  9680  iccid  9991  icoshft  10056  fzen  10109  elfz2nn0  10178  elfzom1p1elfzo  10281  flqeqceilz  10389  zmodidfzoimp  10425  caucvgre  11125  qdenre  11346  dvdsval2  11933  negdvdsb  11950  muldvds2  11960  dvdsabseq  11989  bezoutlemaz  12140  bezoutlembz  12141  rplpwr  12164  alginv  12185  algfx  12190  coprmgcdb  12226  divgcdcoprm0  12239  prmgt1  12270  oddprmgt2  12272  rpexp1i  12292  2sqpwodd  12314  qnumdencl  12325  phiprmpw  12360  prmdiveq  12374  prm23lt5  12401  pcmpt  12481  infpnlem1  12497  oddennn  12549  nninfdclemf1  12609  imasaddfnlemg  12897  aprcotr  13781  cnpnei  14387  bl2in  14571  addcncntoplem  14719  rescncf  14736  limcresi  14820  cnplimcim  14821  efltlemlt  14909  ioocosf1o  14989  uzdcinzz  15290  bj-charfunbi  15303  bj-omssind  15427  bj-bdfindes  15441  bj-nntrans  15443  bj-nnelirr  15445  bj-omtrans  15448  setindis  15459  bdsetindis  15461  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465  bj-findis  15471  bj-findes  15473