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  4592  ralxfrd  4608  ralxfr2d  4610  rexxfr2d  4611  elres  5099  2elresin  5494  f1ocnv  5652  tz6.12c  5725  fvun1  5769  dffo4  5856  isores3  6021  fvdifsuppst  6484  tposfo2  6538  issmo2  6560  iordsmo  6568  smoel2  6574  fiintim  7238  ismkvnex  7495  prarloclemarch  7785  genprndl  7888  genprndu  7889  ltpopr  7962  ltsopr  7963  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprlemu  8007  lttrsr  8129  aptap  8980  rerecapb  9175  nnmulcl  9327  nnnegz  9651  eluzdc  10019  negm  10024  iccid  10337  icoshft  10402  fzen  10457  elfz2nn0  10529  elfzom1p1elfzo  10642  flqeqceilz  10768  zmodidfzoimp  10804  swrd0g  11446  pfxccatin12lem2  11517  swrdccat  11521  swrdccat3blem  11525  caucvgre  11761  qdenre  11983  dvdsval2  12573  negdvdsb  12590  muldvds2  12600  dvdsabseq  12630  bezoutlemaz  12796  bezoutlembz  12797  rplpwr  12820  alginv  12841  algfx  12846  coprmgcdb  12882  divgcdcoprm0  12895  prmgt1  12927  oddprmgt2  12929  rpexp1i  12949  2sqpwodd  12972  qnumdencl  12983  phiprmpw  13020  prmdiveq  13034  prm23lt5  13062  pcmpt  13142  infpnlem1  13158  oddennn  13332  nninfdclemf1  13392  imasaddfnlemg  13684  aprcotr  14646  cnpnei  15369  bl2in  15553  addcncntoplem  15711  rescncf  15731  limcresi  15816  cnplimcim  15817  efltlemlt  15924  ioocosf1o  16005  bposlem1  16209  bposlem5  16213  2lgslem1a1  16303  clwwlkccatlem  16739  clwwlknonex2lem2  16777  uzdcinzz  16924  bj-charfunbi  16935  bj-omssind  17059  bj-bdfindes  17073  bj-nntrans  17075  bj-nnelirr  17077  bj-omtrans  17080  setindis  17091  bdsetindis  17093  bj-inf2vnlem3  17096  bj-inf2vnlem4  17097  bj-findis  17103  bj-findes  17105