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  691  biorf  751  biorfi  753  pm4.72  834  con34bdc  878  notnotbdc  879  dfandc  891  imanst  895  dfordc  899  dfor2dc  902  pm4.79dc  910  orimdidc  913  pm5.54dc  925  pm5.62dc  953  bimsc1  971  dfifp2dc  989  modc  2123  euan  2136  exmoeudc  2143  nebidc  2482  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  elab3gf  2956  abidnf  2974  elsn2g  3702  difsn  3810  prel12  3854  dfnfc2  3911  intmin4  3956  dfiin2g  4003  elpw2g  4246  ordsucg  4600  ssrel  4814  ssrel2  4816  ssrelrel  4826  releldmb  4969  relelrnb  4970  cnveqb  5192  dmsnopg  5208  relcnvtr  5256  relcnvexb  5276  f1ocnvb  5597  ffvresb  5810  fconstfvm  5872  fnoprabg  6122  dfsmo2  6453  nntri2  6662  nntri1  6664  en1bg  6974  pw2f1odclem  7020  fieq0  7175  djulclb  7254  ismkvnex  7354  nngt1ne1  9178  znegclb  9512  iccneg  10224  fzsn  10301  fz1sbc  10331  fzofzp1b  10474  ceilqidz  10579  flqeqceilz  10581  reim0b  11440  rexanre  11798  dvdsext  12434  zob  12470  pc11  12922  pcz  12923  gsumval2  13498  issubg2m  13794  issubg4m  13798  ghmmhmb  13859  opprrngbg  14110  opprringbg  14112  issubrng2  14243  issubrg2  14274  eltg3  14800  bastop  14818  cnptoprest  14982  cos11  15596  zabsle1  15747  lgsabs1  15787  lgsquadlem2  15826  issubgr2  16128  uhgrissubgr  16131  clwwlknun  16311  bj-om  16583  qdiff  16704