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  675  biorf  734  biorfi  736  pm4.72  817  con34bdc  861  notnotbdc  862  dfandc  874  imanst  878  dfordc  882  dfor2dc  885  pm4.79dc  893  orimdidc  896  pm5.54dc  908  pm5.62dc  934  bimsc1  952  modc  2056  euan  2069  exmoeudc  2076  nebidc  2414  cgsexg  2756  cgsex2g  2757  cgsex4g  2758  elab3gf  2871  abidnf  2889  elsn2g  3603  difsn  3704  prel12  3745  dfnfc2  3801  intmin4  3846  dfiin2g  3893  elpw2g  4129  ordsucg  4473  ssrel  4686  ssrel2  4688  ssrelrel  4698  releldmb  4835  relelrnb  4836  cnveqb  5053  dmsnopg  5069  relcnvtr  5117  relcnvexb  5137  f1ocnvb  5440  ffvresb  5642  fconstfvm  5697  fnoprabg  5934  dfsmo2  6246  nntri2  6453  nntri1  6455  en1bg  6757  fieq0  6932  djulclb  7011  ismkvnex  7110  nngt1ne1  8883  znegclb  9215  iccneg  9916  fzsn  9991  fz1sbc  10021  fzofzp1b  10153  ceilqidz  10241  flqeqceilz  10243  reim0b  10790  rexanre  11148  dvdsext  11778  zob  11813  pc11  12239  pcz  12240  eltg3  12598  bastop  12616  cnptoprest  12780  cos11  13315  bj-om  13654