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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimtrrdi  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  683  mtbii  685  orbi2d  802  pm3.11dc  970  prlem1  986  nfimd  1638  dral1  1783  cbvalv1  1804  cbvalh  1806  ax16i  1911  speiv  1915  a16g  1917  cbvalvw  1975  cbvexvw  1976  cleqh  2338  pm13.18  2501  rspcimdv  2930  rspcimedv  2931  rspcedv  2933  moi2  3007  moi  3009  eqrd  3266  ifeqeqxdc  3687  rabsnifsb  3777  abnexg  4594  ralxfrd  4610  ralxfr2d  4612  rexxfr2d  4613  elres  5101  2elresin  5497  f1ocnv  5655  tz6.12c  5728  fvun1  5772  dffo4  5859  isores3  6024  fvdifsuppst  6488  tposfo2  6542  issmo2  6564  iordsmo  6572  smoel2  6578  fiintim  7242  ismkvnex  7501  prarloclemarch  7791  genprndl  7894  genprndu  7895  ltpopr  7968  ltsopr  7969  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprlemu  8013  lttrsr  8135  aptap  8986  rerecapb  9181  nnmulcl  9334  nnnegz  9658  eluzdc  10026  negm  10031  iccid  10344  icoshft  10409  fzen  10464  elfz2nn0  10536  elfzom1p1elfzo  10649  flqeqceilz  10776  zmodidfzoimp  10812  swrd0g  11454  pfxccatin12lem2  11525  swrdccat  11529  swrdccat3blem  11533  caucvgre  11769  qdenre  11991  dvdsval2  12582  negdvdsb  12599  muldvds2  12609  dvdsabseq  12639  bezoutlemaz  12805  bezoutlembz  12806  rplpwr  12829  alginv  12850  algfx  12855  coprmgcdb  12891  divgcdcoprm0  12904  prmgt1  12936  oddprmgt2  12938  rpexp1i  12958  2sqpwodd  12981  qnumdencl  12992  phiprmpw  13029  prmdiveq  13043  prm23lt5  13071  pcmpt  13151  infpnlem1  13167  oddennn  13341  nninfdclemf1  13401  imasaddfnlemg  13694  aprcotr  14706  cnpnei  15445  bl2in  15629  addcncntoplem  15787  rescncf  15807  limcresi  15892  cnplimcim  15893  efltlemlt  16000  ioocosf1o  16082  bposlem1  16311  bposlem5  16315  2lgslem1a1  16410  clwwlkccatlem  16846  clwwlknonex2lem2  16884  uzdcinzz  17031  bj-charfunbi  17042  bj-omssind  17166  bj-bdfindes  17180  bj-nntrans  17182  bj-nnelirr  17184  bj-omtrans  17187  setindis  17198  bdsetindis  17200  bj-inf2vnlem3  17203  bj-inf2vnlem4  17204  bj-findis  17210  bj-findes  17212