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  667  mtbii  669  orbi2d  785  pm4.55dc  933  pm3.11dc  952  prlem1  968  nfimd  1578  dral1  1723  cbvalv1  1744  cbvalh  1746  ax16i  1851  speiv  1855  a16g  1857  cbvalvw  1912  cbvexvw  1913  cleqh  2270  pm13.18  2421  rspcimdv  2835  rspcimedv  2836  rspcedv  2838  moi2  2911  moi  2913  eqrd  3165  abnexg  4431  ralxfrd  4447  ralxfr2d  4449  rexxfr2d  4450  elres  4927  2elresin  5309  f1ocnv  5455  tz6.12c  5526  fvun1  5562  dffo4  5644  isores3  5794  tposfo2  6246  issmo2  6268  iordsmo  6276  smoel2  6282  fiintim  6906  ismkvnex  7131  prarloclemarch  7380  genprndl  7483  genprndu  7484  ltpopr  7557  ltsopr  7558  recexprlem1ssl  7595  recexprlem1ssu  7596  aptiprlemu  7602  lttrsr  7724  nnmulcl  8899  nnnegz  9215  eluzdc  9569  negm  9574  iccid  9882  icoshft  9947  fzen  9999  elfz2nn0  10068  elfzom1p1elfzo  10170  flqeqceilz  10274  zmodidfzoimp  10310  caucvgre  10945  qdenre  11166  dvdsval2  11752  negdvdsb  11769  muldvds2  11779  dvdsabseq  11807  bezoutlemaz  11958  bezoutlembz  11959  rplpwr  11982  alginv  12001  algfx  12006  coprmgcdb  12042  divgcdcoprm0  12055  prmgt1  12086  oddprmgt2  12088  rpexp1i  12108  2sqpwodd  12130  qnumdencl  12141  phiprmpw  12176  prmdiveq  12190  prm23lt5  12217  pcmpt  12295  infpnlem1  12311  oddennn  12347  nninfdclemf1  12407  cnpnei  13013  bl2in  13197  addcncntoplem  13345  rescncf  13362  limcresi  13429  cnplimcim  13430  efltlemlt  13489  ioocosf1o  13569  uzdcinzz  13833  bj-charfunbi  13846  bj-omssind  13970  bj-bdfindes  13984  bj-nntrans  13986  bj-nnelirr  13988  bj-omtrans  13991  setindis  14002  bdsetindis  14004  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008  bj-findis  14014  bj-findes  14016