Theorem impbid2 143

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 142	. 2 |- ( ph -> ( ch <-> ps ) )
4	3	bicomd 141	1 |- ( ph -> ( ps <-> ch ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimt  241  mtt  686  biorf  745  biorfi  747  pm4.72  828  con34bdc  872  notnotbdc  873  dfandc  885  imanst  889  dfordc  893  dfor2dc  896  pm4.79dc  904  orimdidc  907  pm5.54dc  919  pm5.62dc  947  bimsc1  965  modc  2088  euan  2101  exmoeudc  2108  nebidc  2447  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  elab3gf  2914  abidnf  2932  elsn2g  3656  difsn  3760  prel12  3802  dfnfc2  3858  intmin4  3903  dfiin2g  3950  elpw2g  4190  ordsucg  4539  ssrel  4752  ssrel2  4754  ssrelrel  4764  releldmb  4904  relelrnb  4905  cnveqb  5126  dmsnopg  5142  relcnvtr  5190  relcnvexb  5210  f1ocnvb  5521  ffvresb  5728  fconstfvm  5783  fnoprabg  6027  dfsmo2  6354  nntri2  6561  nntri1  6563  en1bg  6868  pw2f1odclem  6904  fieq0  7051  djulclb  7130  ismkvnex  7230  nngt1ne1  9042  znegclb  9376  iccneg  10081  fzsn  10158  fz1sbc  10188  fzofzp1b  10321  ceilqidz  10425  flqeqceilz  10427  reim0b  11044  rexanre  11402  dvdsext  12037  zob  12073  pc11  12525  pcz  12526  gsumval2  13099  issubg2m  13395  issubg4m  13399  ghmmhmb  13460  opprrngbg  13710  opprringbg  13712  issubrng2  13842  issubrg2  13873  eltg3  14377  bastop  14395  cnptoprest  14559  cos11  15173  zabsle1  15324  lgsabs1  15364  lgsquadlem2  15403  bj-om  15667