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  685  biorf  744  biorfi  746  pm4.72  827  con34bdc  871  notnotbdc  872  dfandc  884  imanst  888  dfordc  892  dfor2dc  895  pm4.79dc  903  orimdidc  906  pm5.54dc  918  pm5.62dc  945  bimsc1  963  modc  2069  euan  2082  exmoeudc  2089  nebidc  2427  cgsexg  2774  cgsex2g  2775  cgsex4g  2776  elab3gf  2889  abidnf  2907  elsn2g  3627  difsn  3731  prel12  3773  dfnfc2  3829  intmin4  3874  dfiin2g  3921  elpw2g  4158  ordsucg  4503  ssrel  4716  ssrel2  4718  ssrelrel  4728  releldmb  4866  relelrnb  4867  cnveqb  5086  dmsnopg  5102  relcnvtr  5150  relcnvexb  5170  f1ocnvb  5477  ffvresb  5681  fconstfvm  5736  fnoprabg  5978  dfsmo2  6290  nntri2  6497  nntri1  6499  en1bg  6802  fieq0  6977  djulclb  7056  ismkvnex  7155  nngt1ne1  8956  znegclb  9288  iccneg  9991  fzsn  10068  fz1sbc  10098  fzofzp1b  10230  ceilqidz  10318  flqeqceilz  10320  reim0b  10873  rexanre  11231  dvdsext  11863  zob  11898  pc11  12332  pcz  12333  issubg2m  13054  issubg4m  13058  opprringbg  13255  issubrg2  13367  eltg3  13596  bastop  13614  cnptoprest  13778  cos11  14313  zabsle1  14439  lgsabs1  14479  bj-om  14728