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  935  bimsc1  953  modc  2057  euan  2070  exmoeudc  2077  nebidc  2416  cgsexg  2761  cgsex2g  2762  cgsex4g  2763  elab3gf  2876  abidnf  2894  elsn2g  3609  difsn  3710  prel12  3751  dfnfc2  3807  intmin4  3852  dfiin2g  3899  elpw2g  4135  ordsucg  4479  ssrel  4692  ssrel2  4694  ssrelrel  4704  releldmb  4841  relelrnb  4842  cnveqb  5059  dmsnopg  5075  relcnvtr  5123  relcnvexb  5143  f1ocnvb  5446  ffvresb  5648  fconstfvm  5703  fnoprabg  5943  dfsmo2  6255  nntri2  6462  nntri1  6464  en1bg  6766  fieq0  6941  djulclb  7020  ismkvnex  7119  nngt1ne1  8892  znegclb  9224  iccneg  9925  fzsn  10001  fz1sbc  10031  fzofzp1b  10163  ceilqidz  10251  flqeqceilz  10253  reim0b  10804  rexanre  11162  dvdsext  11793  zob  11828  pc11  12262  pcz  12263  eltg3  12697  bastop  12715  cnptoprest  12879  cos11  13414  zabsle1  13540  lgsabs1  13580  bj-om  13819