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  676  mtbii  678  orbi2d  795  pm3.11dc  963  prlem1  979  nfimd  1631  dral1  1776  cbvalv1  1797  cbvalh  1799  ax16i  1904  speiv  1908  a16g  1910  cbvalvw  1966  cbvexvw  1967  cleqh  2329  pm13.18  2481  rspcimdv  2909  rspcimedv  2910  rspcedv  2912  moi2  2985  moi  2987  eqrd  3243  rabsnifsb  3735  abnexg  4541  ralxfrd  4557  ralxfr2d  4559  rexxfr2d  4560  elres  5047  2elresin  5440  f1ocnv  5593  tz6.12c  5665  fvun1  5708  dffo4  5791  isores3  5951  tposfo2  6428  issmo2  6450  iordsmo  6458  smoel2  6464  fiintim  7116  ismkvnex  7345  prarloclemarch  7628  genprndl  7731  genprndu  7732  ltpopr  7805  ltsopr  7806  recexprlem1ssl  7843  recexprlem1ssu  7844  aptiprlemu  7850  lttrsr  7972  aptap  8820  rerecapb  9013  nnmulcl  9154  nnnegz  9472  eluzdc  9834  negm  9839  iccid  10150  icoshft  10215  fzen  10268  elfz2nn0  10337  elfzom1p1elfzo  10449  flqeqceilz  10570  zmodidfzoimp  10606  swrd0g  11231  pfxccatin12lem2  11302  swrdccat  11306  swrdccat3blem  11310  caucvgre  11532  qdenre  11753  dvdsval2  12341  negdvdsb  12358  muldvds2  12368  dvdsabseq  12398  bezoutlemaz  12564  bezoutlembz  12565  rplpwr  12588  alginv  12609  algfx  12614  coprmgcdb  12650  divgcdcoprm0  12663  prmgt1  12694  oddprmgt2  12696  rpexp1i  12716  2sqpwodd  12738  qnumdencl  12749  phiprmpw  12784  prmdiveq  12798  prm23lt5  12826  pcmpt  12906  infpnlem1  12922  oddennn  13003  nninfdclemf1  13063  imasaddfnlemg  13387  aprcotr  14289  cnpnei  14933  bl2in  15117  addcncntoplem  15275  rescncf  15295  limcresi  15380  cnplimcim  15381  efltlemlt  15488  ioocosf1o  15568  2lgslem1a1  15805  clwwlkccatlem  16195  clwwlknonex2lem2  16233  uzdcinzz  16330  bj-charfunbi  16342  bj-omssind  16466  bj-bdfindes  16480  bj-nntrans  16482  bj-nnelirr  16484  bj-omtrans  16487  setindis  16498  bdsetindis  16500  bj-inf2vnlem3  16503  bj-inf2vnlem4  16504  bj-findis  16510  bj-findes  16512