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  3614  difsn  3715  prel12  3756  dfnfc2  3812  intmin4  3857  dfiin2g  3904  elpw2g  4140  ordsucg  4484  ssrel  4697  ssrel2  4699  ssrelrel  4709  releldmb  4846  relelrnb  4847  cnveqb  5064  dmsnopg  5080  relcnvtr  5128  relcnvexb  5148  f1ocnvb  5454  ffvresb  5657  fconstfvm  5712  fnoprabg  5952  dfsmo2  6264  nntri2  6471  nntri1  6473  en1bg  6775  fieq0  6950  djulclb  7029  ismkvnex  7128  nngt1ne1  8902  znegclb  9234  iccneg  9935  fzsn  10011  fz1sbc  10041  fzofzp1b  10173  ceilqidz  10261  flqeqceilz  10263  reim0b  10815  rexanre  11173  dvdsext  11804  zob  11839  pc11  12273  pcz  12274  eltg3  12812  bastop  12830  cnptoprest  12994  cos11  13529  zabsle1  13655  lgsabs1  13695  bj-om  13934