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  689  biorf  749  biorfi  751  pm4.72  832  con34bdc  876  notnotbdc  877  dfandc  889  imanst  893  dfordc  897  dfor2dc  900  pm4.79dc  908  orimdidc  911  pm5.54dc  923  pm5.62dc  951  bimsc1  969  dfifp2dc  987  modc  2121  euan  2134  exmoeudc  2141  nebidc  2480  cgsexg  2835  cgsex2g  2836  cgsex4g  2837  elab3gf  2953  abidnf  2971  elsn2g  3699  difsn  3805  prel12  3849  dfnfc2  3906  intmin4  3951  dfiin2g  3998  elpw2g  4240  ordsucg  4594  ssrel  4807  ssrel2  4809  ssrelrel  4819  releldmb  4961  relelrnb  4962  cnveqb  5184  dmsnopg  5200  relcnvtr  5248  relcnvexb  5268  f1ocnvb  5586  ffvresb  5798  fconstfvm  5857  fnoprabg  6105  dfsmo2  6433  nntri2  6640  nntri1  6642  en1bg  6952  pw2f1odclem  6995  fieq0  7143  djulclb  7222  ismkvnex  7322  nngt1ne1  9145  znegclb  9479  iccneg  10185  fzsn  10262  fz1sbc  10292  fzofzp1b  10434  ceilqidz  10538  flqeqceilz  10540  reim0b  11373  rexanre  11731  dvdsext  12366  zob  12402  pc11  12854  pcz  12855  gsumval2  13430  issubg2m  13726  issubg4m  13730  ghmmhmb  13791  opprrngbg  14041  opprringbg  14043  issubrng2  14174  issubrg2  14205  eltg3  14731  bastop  14749  cnptoprest  14913  cos11  15527  zabsle1  15678  lgsabs1  15718  lgsquadlem2  15757  bj-om  16300