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-mp 5  ax-1 6  ax-2 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  295  mtbid  661  mtbii  663  orbi2d  779  pm4.55dc  922  pm3.11dc  941  prlem1  957  nfimd  1564  dral1  1708  cbvalh  1726  ax16i  1830  speiv  1834  a16g  1836  cleqh  2237  pm13.18  2387  rspcimdv  2785  rspcimedv  2786  rspcedv  2788  moi2  2860  moi  2862  eqrd  3110  abnexg  4362  ralxfrd  4378  ralxfr2d  4380  rexxfr2d  4381  elres  4850  2elresin  5229  f1ocnv  5373  tz6.12c  5444  fvun1  5480  dffo4  5561  isores3  5709  tposfo2  6157  issmo2  6179  iordsmo  6187  smoel2  6193  fiintim  6810  ismkvnex  7022  prarloclemarch  7219  genprndl  7322  genprndu  7323  ltpopr  7396  ltsopr  7397  recexprlem1ssl  7434  recexprlem1ssu  7435  aptiprlemu  7441  lttrsr  7563  nnmulcl  8734  nnnegz  9050  eluzdc  9397  negm  9400  iccid  9701  icoshft  9766  fzen  9816  elfz2nn0  9885  elfzom1p1elfzo  9984  flqeqceilz  10084  zmodidfzoimp  10120  caucvgre  10746  qdenre  10967  dvdsval2  11485  negdvdsb  11498  muldvds2  11508  dvdsabseq  11534  bezoutlemaz  11680  bezoutlembz  11681  rplpwr  11704  alginv  11717  algfx  11722  coprmgcdb  11758  divgcdcoprm0  11771  prmgt1  11801  oddprmgt2  11803  rpexp1i  11821  2sqpwodd  11843  qnumdencl  11854  phiprmpw  11887  oddennn  11894  cnpnei  12377  bl2in  12561  addcncntoplem  12709  rescncf  12726  limcresi  12793  cnplimcim  12794  uzdcinzz  12994  bj-omssind  13122  bj-bdfindes  13136  bj-nntrans  13138  bj-nnelirr  13140  bj-omtrans  13143  setindis  13154  bdsetindis  13156  bj-inf2vnlem3  13159  bj-inf2vnlem4  13160  bj-findis  13166  bj-findes  13168