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  679  mtbii  681  orbi2d  798  pm3.11dc  966  prlem1  982  nfimd  1634  dral1  1779  cbvalv1  1800  cbvalh  1802  ax16i  1907  speiv  1911  a16g  1913  cbvalvw  1971  cbvexvw  1972  cleqh  2334  pm13.18  2495  rspcimdv  2924  rspcimedv  2925  rspcedv  2927  moi2  3000  moi  3002  eqrd  3258  rabsnifsb  3759  abnexg  4569  ralxfrd  4585  ralxfr2d  4587  rexxfr2d  4588  elres  5076  2elresin  5471  f1ocnv  5629  tz6.12c  5702  fvun1  5745  dffo4  5827  isores3  5990  fvdifsuppst  6446  tposfo2  6500  issmo2  6522  iordsmo  6530  smoel2  6536  fiintim  7193  ismkvnex  7448  prarloclemarch  7735  genprndl  7838  genprndu  7839  ltpopr  7912  ltsopr  7913  recexprlem1ssl  7950  recexprlem1ssu  7951  aptiprlemu  7957  lttrsr  8079  aptap  8926  rerecapb  9119  nnmulcl  9260  nnnegz  9582  eluzdc  9945  negm  9950  iccid  10261  icoshft  10326  fzen  10380  elfz2nn0  10450  elfzom1p1elfzo  10563  flqeqceilz  10684  zmodidfzoimp  10720  swrd0g  11356  pfxccatin12lem2  11427  swrdccat  11431  swrdccat3blem  11435  caucvgre  11670  qdenre  11891  dvdsval2  12480  negdvdsb  12497  muldvds2  12507  dvdsabseq  12537  bezoutlemaz  12703  bezoutlembz  12704  rplpwr  12727  alginv  12748  algfx  12753  coprmgcdb  12789  divgcdcoprm0  12802  prmgt1  12833  oddprmgt2  12835  rpexp1i  12855  2sqpwodd  12877  qnumdencl  12888  phiprmpw  12923  prmdiveq  12937  prm23lt5  12965  pcmpt  13045  infpnlem1  13061  oddennn  13160  nninfdclemf1  13220  imasaddfnlemg  13544  aprcotr  14448  cnpnei  15101  bl2in  15285  addcncntoplem  15443  rescncf  15463  limcresi  15548  cnplimcim  15549  efltlemlt  15656  ioocosf1o  15736  2lgslem1a1  15976  clwwlkccatlem  16412  clwwlknonex2lem2  16450  uzdcinzz  16587  bj-charfunbi  16598  bj-omssind  16722  bj-bdfindes  16736  bj-nntrans  16738  bj-nnelirr  16740  bj-omtrans  16743  setindis  16754  bdsetindis  16756  bj-inf2vnlem3  16759  bj-inf2vnlem4  16760  bj-findis  16766  bj-findes  16768