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  678  mtbii  680  orbi2d  797  pm3.11dc  965  prlem1  981  nfimd  1633  dral1  1778  cbvalv1  1799  cbvalh  1801  ax16i  1906  speiv  1910  a16g  1912  cbvalvw  1968  cbvexvw  1969  cleqh  2331  pm13.18  2483  rspcimdv  2911  rspcimedv  2912  rspcedv  2914  moi2  2987  moi  2989  eqrd  3245  rabsnifsb  3737  abnexg  4543  ralxfrd  4559  ralxfr2d  4561  rexxfr2d  4562  elres  5049  2elresin  5443  f1ocnv  5596  tz6.12c  5669  fvun1  5712  dffo4  5795  isores3  5956  tposfo2  6433  issmo2  6455  iordsmo  6463  smoel2  6469  fiintim  7123  ismkvnex  7354  prarloclemarch  7638  genprndl  7741  genprndu  7742  ltpopr  7815  ltsopr  7816  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprlemu  7860  lttrsr  7982  aptap  8830  rerecapb  9023  nnmulcl  9164  nnnegz  9482  eluzdc  9844  negm  9849  iccid  10160  icoshft  10225  fzen  10278  elfz2nn0  10347  elfzom1p1elfzo  10460  flqeqceilz  10581  zmodidfzoimp  10617  swrd0g  11245  pfxccatin12lem2  11316  swrdccat  11320  swrdccat3blem  11324  caucvgre  11559  qdenre  11780  dvdsval2  12369  negdvdsb  12386  muldvds2  12396  dvdsabseq  12426  bezoutlemaz  12592  bezoutlembz  12593  rplpwr  12616  alginv  12637  algfx  12642  coprmgcdb  12678  divgcdcoprm0  12691  prmgt1  12722  oddprmgt2  12724  rpexp1i  12744  2sqpwodd  12766  qnumdencl  12777  phiprmpw  12812  prmdiveq  12826  prm23lt5  12854  pcmpt  12934  infpnlem1  12950  oddennn  13031  nninfdclemf1  13091  imasaddfnlemg  13415  aprcotr  14318  cnpnei  14962  bl2in  15146  addcncntoplem  15304  rescncf  15324  limcresi  15409  cnplimcim  15410  efltlemlt  15517  ioocosf1o  15597  2lgslem1a1  15834  clwwlkccatlem  16270  clwwlknonex2lem2  16308  uzdcinzz  16445  bj-charfunbi  16457  bj-omssind  16581  bj-bdfindes  16595  bj-nntrans  16597  bj-nnelirr  16599  bj-omtrans  16602  setindis  16613  bdsetindis  16615  bj-inf2vnlem3  16618  bj-inf2vnlem4  16619  bj-findis  16625  bj-findes  16627