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  946  bimsc1  964  modc  2080  euan  2093  exmoeudc  2100  nebidc  2439  cgsexg  2786  cgsex2g  2787  cgsex4g  2788  elab3gf  2901  abidnf  2919  elsn2g  3639  difsn  3743  prel12  3785  dfnfc2  3841  intmin4  3886  dfiin2g  3933  elpw2g  4170  ordsucg  4515  ssrel  4728  ssrel2  4730  ssrelrel  4740  releldmb  4878  relelrnb  4879  cnveqb  5098  dmsnopg  5114  relcnvtr  5162  relcnvexb  5182  f1ocnvb  5489  ffvresb  5694  fconstfvm  5749  fnoprabg  5991  dfsmo2  6305  nntri2  6512  nntri1  6514  en1bg  6817  fieq0  6992  djulclb  7071  ismkvnex  7170  nngt1ne1  8971  znegclb  9303  iccneg  10006  fzsn  10083  fz1sbc  10113  fzofzp1b  10245  ceilqidz  10333  flqeqceilz  10335  reim0b  10888  rexanre  11246  dvdsext  11878  zob  11913  pc11  12347  pcz  12348  issubg2m  13093  issubg4m  13097  ghmmhmb  13153  opprrngbg  13388  opprringbg  13390  issubrng2  13517  issubrg2  13548  eltg3  13940  bastop  13958  cnptoprest  14122  cos11  14657  zabsle1  14783  lgsabs1  14823  bj-om  15072