Theorem biimprd 156

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	syl5ibr 154	1 |- ( ph -> ( ch -> ps ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl6bir  162  mpbird  165  sylibrd  167  sylbird  168  imbi1d  229  biimpar  291  notbid  624  mtbid  629  mtbii  631  orbi2d  736  pm4.55dc  879  pm3.11dc  898  prlem1  914  nfimd  1517  dral1  1658  cbvalh  1676  ax16i  1779  speiv  1783  a16g  1785  cleqh  2178  pm13.18  2326  rspcimdv  2702  rspcimedv  2703  rspcedv  2705  moi2  2773  moi  2775  eqrd  3017  ralxfrd  4212  ralxfr2d  4214  rexxfr2d  4215  elres  4664  2elresin  5030  f1ocnv  5159  tz6.12c  5224  fvun1  5260  dffo4  5336  isores3  5475  tposfo2  5905  issmo2  5927  iordsmo  5935  smoel2  5941  prarloclemarch  6608  genprndl  6711  genprndu  6712  ltpopr  6785  ltsopr  6786  recexprlem1ssl  6823  recexprlem1ssu  6824  aptiprlemu  6830  lttrsr  6939  nnmulcl  8060  nnnegz  8354  eluzdc  8697  negm  8700  iccid  8948  icoshft  9012  fzen  9062  elfz2nn0  9128  elfzom1p1elfzo  9223  flqeqceilz  9320  zmodidfzoimp  9356  caucvgre  9867  qdenre  10088  dvdsval2  10198  negdvdsb  10211  muldvds2  10221  dvdsabseq  10247  bezoutlemaz  10392  bezoutlembz  10393  rplpwr  10416  ialginv  10429  ialgfx  10434  coprmgcdb  10470  divgcdcoprm0  10483  prmgt1  10513  oddprmgt2  10515  rpexp1i  10533  2sqpwodd  10554  bj-omssind  10730  bj-bdfindes  10744  bj-nntrans  10746  bj-nnelirr  10748  bj-omtrans  10751  setindis  10762  bdsetindis  10764  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768  bj-findis  10774  bj-findes  10776