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  674  biorf  733  biorfi  735  pm4.72  812  biort  814  con34bdc  856  notnotbdc  857  dfandc  869  imanst  873  dfordc  877  dfor2dc  880  pm4.79dc  888  orimdidc  891  pm5.54dc  903  pm5.62dc  929  bimsc1  947  modc  2042  euan  2055  exmoeudc  2062  nebidc  2388  cgsexg  2721  cgsex2g  2722  cgsex4g  2723  elab3gf  2834  abidnf  2852  elsn2g  3558  difsn  3657  prel12  3698  dfnfc2  3754  intmin4  3799  dfiin2g  3846  elpw2g  4081  ordsucg  4418  ssrel  4627  ssrel2  4629  ssrelrel  4639  releldmb  4776  relelrnb  4777  cnveqb  4994  dmsnopg  5010  relcnvtr  5058  relcnvexb  5078  f1ocnvb  5381  ffvresb  5583  fconstfvm  5638  fnoprabg  5872  dfsmo2  6184  nntri2  6390  nntri1  6392  en1bg  6694  fieq0  6864  djulclb  6940  ismkvnex  7029  nngt1ne1  8755  znegclb  9087  iccneg  9772  fzsn  9846  fz1sbc  9876  fzofzp1b  10005  ceilqidz  10089  flqeqceilz  10091  reim0b  10634  rexanre  10992  dvdsext  11553  zob  11588  eltg3  12226  bastop  12244  cnptoprest  12408  bj-om  13135