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:  biimtrrdi  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  676  mtbii  678  orbi2d  795  pm3.11dc  963  prlem1  979  nfimd  1631  dral1  1776  cbvalv1  1797  cbvalh  1799  ax16i  1904  speiv  1908  a16g  1910  cbvalvw  1966  cbvexvw  1967  cleqh  2329  pm13.18  2481  rspcimdv  2908  rspcimedv  2909  rspcedv  2911  moi2  2984  moi  2986  eqrd  3242  abnexg  4537  ralxfrd  4553  ralxfr2d  4555  rexxfr2d  4556  elres  5041  2elresin  5434  f1ocnv  5585  tz6.12c  5657  fvun1  5700  dffo4  5783  isores3  5939  tposfo2  6413  issmo2  6435  iordsmo  6443  smoel2  6449  fiintim  7093  ismkvnex  7322  prarloclemarch  7605  genprndl  7708  genprndu  7709  ltpopr  7782  ltsopr  7783  recexprlem1ssl  7820  recexprlem1ssu  7821  aptiprlemu  7827  lttrsr  7949  aptap  8797  rerecapb  8990  nnmulcl  9131  nnnegz  9449  eluzdc  9805  negm  9810  iccid  10121  icoshft  10186  fzen  10239  elfz2nn0  10308  elfzom1p1elfzo  10420  flqeqceilz  10540  zmodidfzoimp  10576  swrd0g  11192  pfxccatin12lem2  11263  swrdccat  11267  swrdccat3blem  11271  caucvgre  11492  qdenre  11713  dvdsval2  12301  negdvdsb  12318  muldvds2  12328  dvdsabseq  12358  bezoutlemaz  12524  bezoutlembz  12525  rplpwr  12548  alginv  12569  algfx  12574  coprmgcdb  12610  divgcdcoprm0  12623  prmgt1  12654  oddprmgt2  12656  rpexp1i  12676  2sqpwodd  12698  qnumdencl  12709  phiprmpw  12744  prmdiveq  12758  prm23lt5  12786  pcmpt  12866  infpnlem1  12882  oddennn  12963  nninfdclemf1  13023  imasaddfnlemg  13347  aprcotr  14249  cnpnei  14893  bl2in  15077  addcncntoplem  15235  rescncf  15255  limcresi  15340  cnplimcim  15341  efltlemlt  15448  ioocosf1o  15528  2lgslem1a1  15765  uzdcinzz  16162  bj-charfunbi  16174  bj-omssind  16298  bj-bdfindes  16312  bj-nntrans  16314  bj-nnelirr  16316  bj-omtrans  16319  setindis  16330  bdsetindis  16332  bj-inf2vnlem3  16335  bj-inf2vnlem4  16336  bj-findis  16342  bj-findes  16344