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:  syl6bir  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  673  mtbii  675  orbi2d  791  pm4.55dc  939  pm3.11dc  958  prlem1  974  nfimd  1595  dral1  1740  cbvalv1  1761  cbvalh  1763  ax16i  1868  speiv  1872  a16g  1874  cbvalvw  1929  cbvexvw  1930  cleqh  2287  pm13.18  2438  rspcimdv  2854  rspcimedv  2855  rspcedv  2857  moi2  2930  moi  2932  eqrd  3185  abnexg  4458  ralxfrd  4474  ralxfr2d  4476  rexxfr2d  4477  elres  4955  2elresin  5339  f1ocnv  5486  tz6.12c  5557  fvun1  5595  dffo4  5677  isores3  5829  tposfo2  6282  issmo2  6304  iordsmo  6312  smoel2  6318  fiintim  6942  ismkvnex  7167  prarloclemarch  7431  genprndl  7534  genprndu  7535  ltpopr  7608  ltsopr  7609  recexprlem1ssl  7646  recexprlem1ssu  7647  aptiprlemu  7653  lttrsr  7775  aptap  8621  rerecapb  8814  nnmulcl  8954  nnnegz  9270  eluzdc  9624  negm  9629  iccid  9939  icoshft  10004  fzen  10057  elfz2nn0  10126  elfzom1p1elfzo  10228  flqeqceilz  10332  zmodidfzoimp  10368  caucvgre  11004  qdenre  11225  dvdsval2  11811  negdvdsb  11828  muldvds2  11838  dvdsabseq  11867  bezoutlemaz  12018  bezoutlembz  12019  rplpwr  12042  alginv  12061  algfx  12066  coprmgcdb  12102  divgcdcoprm0  12115  prmgt1  12146  oddprmgt2  12148  rpexp1i  12168  2sqpwodd  12190  qnumdencl  12201  phiprmpw  12236  prmdiveq  12250  prm23lt5  12277  pcmpt  12355  infpnlem1  12371  oddennn  12407  nninfdclemf1  12467  imasaddfnlemg  12753  aprcotr  13474  cnpnei  14015  bl2in  14199  addcncntoplem  14347  rescncf  14364  limcresi  14431  cnplimcim  14432  efltlemlt  14491  ioocosf1o  14571  uzdcinzz  14846  bj-charfunbi  14859  bj-omssind  14983  bj-bdfindes  14997  bj-nntrans  14999  bj-nnelirr  15001  bj-omtrans  15004  setindis  15015  bdsetindis  15017  bj-inf2vnlem3  15020  bj-inf2vnlem4  15021  bj-findis  15027  bj-findes  15029