Theorem biimprd 157

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	syl5ibr 155	1 |- ( ph -> ( ch -> ps ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl6bir  163  mpbird  166  sylibrd  168  sylbird  169  imbi1d  230  biimpar  293  notbid  633  mtbid  638  mtbii  640  orbi2d  745  pm4.55dc  890  pm3.11dc  909  prlem1  925  nfimd  1532  dral1  1676  cbvalh  1694  ax16i  1797  speiv  1801  a16g  1803  cleqh  2199  pm13.18  2348  rspcimdv  2745  rspcimedv  2746  rspcedv  2748  moi2  2818  moi  2820  eqrd  3065  abnexg  4305  ralxfrd  4321  ralxfr2d  4323  rexxfr2d  4324  elres  4791  2elresin  5170  f1ocnv  5314  tz6.12c  5383  fvun1  5419  dffo4  5500  isores3  5648  tposfo2  6094  issmo2  6116  iordsmo  6124  smoel2  6130  fiintim  6746  prarloclemarch  7127  genprndl  7230  genprndu  7231  ltpopr  7304  ltsopr  7305  recexprlem1ssl  7342  recexprlem1ssu  7343  aptiprlemu  7349  lttrsr  7458  nnmulcl  8599  nnnegz  8909  eluzdc  9254  negm  9257  iccid  9549  icoshft  9614  fzen  9664  elfz2nn0  9733  elfzom1p1elfzo  9832  flqeqceilz  9932  zmodidfzoimp  9968  caucvgre  10593  qdenre  10814  dvdsval2  11291  negdvdsb  11304  muldvds2  11314  dvdsabseq  11340  bezoutlemaz  11484  bezoutlembz  11485  rplpwr  11508  alginv  11521  algfx  11526  coprmgcdb  11562  divgcdcoprm0  11575  prmgt1  11605  oddprmgt2  11607  rpexp1i  11625  2sqpwodd  11646  qnumdencl  11657  phiprmpw  11690  oddennn  11697  cnpnei  12169  bl2in  12331  rescncf  12481  limcresi  12515  cnplimcim  12516  uzdcinzz  12586  bj-omssind  12718  bj-bdfindes  12732  bj-nntrans  12734  bj-nnelirr  12736  bj-omtrans  12739  setindis  12750  bdsetindis  12752  bj-inf2vnlem3  12755  bj-inf2vnlem4  12756  bj-findis  12762  bj-findes  12764