Theorem impbid2 142

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)

Hypotheses

Ref	Expression
impbid2.1	|- ( ps -> ch )
impbid2.2	|- ( ph -> ( ch -> ps ) )

Assertion

Ref	Expression
impbid2	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3 |- ( ph -> ( ch -> ps ) )
2		impbid2.1	. . 3 |- ( ps -> ch )
3	1, 2	impbid1 141	. 2 |- ( ph -> ( ch <-> ps ) )
4	3	bicomd 140	1 |- ( ph -> ( ps <-> ch ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimt  240  mtt  680  biorf  739  biorfi  741  pm4.72  822  con34bdc  866  notnotbdc  867  dfandc  879  imanst  883  dfordc  887  dfor2dc  890  pm4.79dc  898  orimdidc  901  pm5.54dc  913  pm5.62dc  940  bimsc1  958  modc  2062  euan  2075  exmoeudc  2082  nebidc  2420  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  elab3gf  2880  abidnf  2898  elsn2g  3616  difsn  3717  prel12  3758  dfnfc2  3814  intmin4  3859  dfiin2g  3906  elpw2g  4142  ordsucg  4486  ssrel  4699  ssrel2  4701  ssrelrel  4711  releldmb  4848  relelrnb  4849  cnveqb  5066  dmsnopg  5082  relcnvtr  5130  relcnvexb  5150  f1ocnvb  5456  ffvresb  5659  fconstfvm  5714  fnoprabg  5954  dfsmo2  6266  nntri2  6473  nntri1  6475  en1bg  6778  fieq0  6953  djulclb  7032  ismkvnex  7131  nngt1ne1  8913  znegclb  9245  iccneg  9946  fzsn  10022  fz1sbc  10052  fzofzp1b  10184  ceilqidz  10272  flqeqceilz  10274  reim0b  10826  rexanre  11184  dvdsext  11815  zob  11850  pc11  12284  pcz  12285  eltg3  12851  bastop  12869  cnptoprest  13033  cos11  13568  zabsle1  13694  lgsabs1  13734  bj-om  13972