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-1 5  ax-2 6  ax-mp 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  651  biorf  704  biorfi  706  pm4.72  778  biort  780  imanst  785  con34bdc  809  notnotbdc  810  dfandc  822  dfordc  835  dfor2dc  838  pm4.79dc  853  orimdidc  856  pm5.54dc  871  pm5.62dc  897  bimsc1  915  modc  2003  euan  2016  exmoeudc  2023  nebidc  2347  cgsexg  2676  cgsex2g  2677  cgsex4g  2678  elab3gf  2787  abidnf  2805  elsn2g  3505  difsn  3604  prel12  3645  dfnfc2  3701  intmin4  3746  dfiin2g  3793  elpw2g  4021  ordsucg  4356  ssrel  4565  ssrel2  4567  ssrelrel  4577  releldmb  4714  relelrnb  4715  cnveqb  4930  dmsnopg  4946  relcnvtr  4994  relcnvexb  5014  f1ocnvb  5315  ffvresb  5515  fconstfvm  5570  fnoprabg  5804  dfsmo2  6114  nntri2  6320  nntri1  6322  en1bg  6624  djulclb  6855  nngt1ne1  8613  znegclb  8939  iccneg  9613  fzsn  9687  fz1sbc  9717  fzofzp1b  9846  ceilqidz  9930  flqeqceilz  9932  reim0b  10475  rexanre  10832  dvdsext  11348  zob  11383  eltg3  12008  bastop  12026  cnptoprest  12189  bj-om  12720