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  662  mtbii  664  orbi2d  780  pm4.55dc  928  pm3.11dc  947  prlem1  963  nfimd  1573  dral1  1718  cbvalv1  1739  cbvalh  1741  ax16i  1846  speiv  1850  a16g  1852  cbvalvw  1907  cbvexvw  1908  cleqh  2266  pm13.18  2417  rspcimdv  2831  rspcimedv  2832  rspcedv  2834  moi2  2907  moi  2909  eqrd  3160  abnexg  4424  ralxfrd  4440  ralxfr2d  4442  rexxfr2d  4443  elres  4920  2elresin  5299  f1ocnv  5445  tz6.12c  5516  fvun1  5552  dffo4  5633  isores3  5783  tposfo2  6235  issmo2  6257  iordsmo  6265  smoel2  6271  fiintim  6894  ismkvnex  7119  prarloclemarch  7359  genprndl  7462  genprndu  7463  ltpopr  7536  ltsopr  7537  recexprlem1ssl  7574  recexprlem1ssu  7575  aptiprlemu  7581  lttrsr  7703  nnmulcl  8878  nnnegz  9194  eluzdc  9548  negm  9553  iccid  9861  icoshft  9926  fzen  9978  elfz2nn0  10047  elfzom1p1elfzo  10149  flqeqceilz  10253  zmodidfzoimp  10289  caucvgre  10923  qdenre  11144  dvdsval2  11730  negdvdsb  11747  muldvds2  11757  dvdsabseq  11785  bezoutlemaz  11936  bezoutlembz  11937  rplpwr  11960  alginv  11979  algfx  11984  coprmgcdb  12020  divgcdcoprm0  12033  prmgt1  12064  oddprmgt2  12066  rpexp1i  12086  2sqpwodd  12108  qnumdencl  12119  phiprmpw  12154  prmdiveq  12168  prm23lt5  12195  pcmpt  12273  infpnlem1  12289  oddennn  12325  nninfdclemf1  12385  cnpnei  12859  bl2in  13043  addcncntoplem  13191  rescncf  13208  limcresi  13275  cnplimcim  13276  efltlemlt  13335  ioocosf1o  13415  uzdcinzz  13679  bj-charfunbi  13693  bj-omssind  13817  bj-bdfindes  13831  bj-nntrans  13833  bj-nnelirr  13835  bj-omtrans  13838  setindis  13849  bdsetindis  13851  bj-inf2vnlem3  13854  bj-inf2vnlem4  13855  bj-findis  13861  bj-findes  13863