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  1599  dral1  1744  cbvalv1  1765  cbvalh  1767  ax16i  1872  speiv  1876  a16g  1878  cbvalvw  1934  cbvexvw  1935  cleqh  2296  pm13.18  2448  rspcimdv  2869  rspcimedv  2870  rspcedv  2872  moi2  2945  moi  2947  eqrd  3202  abnexg  4482  ralxfrd  4498  ralxfr2d  4500  rexxfr2d  4501  elres  4983  2elresin  5372  f1ocnv  5520  tz6.12c  5591  fvun1  5630  dffo4  5713  isores3  5865  tposfo2  6334  issmo2  6356  iordsmo  6364  smoel2  6370  fiintim  7001  ismkvnex  7230  prarloclemarch  7502  genprndl  7605  genprndu  7606  ltpopr  7679  ltsopr  7680  recexprlem1ssl  7717  recexprlem1ssu  7718  aptiprlemu  7724  lttrsr  7846  aptap  8694  rerecapb  8887  nnmulcl  9028  nnnegz  9346  eluzdc  9701  negm  9706  iccid  10017  icoshft  10082  fzen  10135  elfz2nn0  10204  elfzom1p1elfzo  10307  flqeqceilz  10427  zmodidfzoimp  10463  caucvgre  11163  qdenre  11384  dvdsval2  11972  negdvdsb  11989  muldvds2  11999  dvdsabseq  12029  bezoutlemaz  12195  bezoutlembz  12196  rplpwr  12219  alginv  12240  algfx  12245  coprmgcdb  12281  divgcdcoprm0  12294  prmgt1  12325  oddprmgt2  12327  rpexp1i  12347  2sqpwodd  12369  qnumdencl  12380  phiprmpw  12415  prmdiveq  12429  prm23lt5  12457  pcmpt  12537  infpnlem1  12553  oddennn  12634  nninfdclemf1  12694  imasaddfnlemg  13016  aprcotr  13917  cnpnei  14539  bl2in  14723  addcncntoplem  14881  rescncf  14901  limcresi  14986  cnplimcim  14987  efltlemlt  15094  ioocosf1o  15174  2lgslem1a1  15411  uzdcinzz  15528  bj-charfunbi  15541  bj-omssind  15665  bj-bdfindes  15679  bj-nntrans  15681  bj-nnelirr  15683  bj-omtrans  15686  setindis  15697  bdsetindis  15699  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703  bj-findis  15709  bj-findes  15711