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  5588  ffvresb  5800  fconstfvm  5861  fnoprabg  6111  dfsmo2  6439  nntri2  6648  nntri1  6650  en1bg  6960  pw2f1odclem  7003  fieq0  7154  djulclb  7233  ismkvnex  7333  nngt1ne1  9156  znegclb  9490  iccneg  10197  fzsn  10274  fz1sbc  10304  fzofzp1b  10446  ceilqidz  10550  flqeqceilz  10552  reim0b  11389  rexanre  11747  dvdsext  12382  zob  12418  pc11  12870  pcz  12871  gsumval2  13446  issubg2m  13742  issubg4m  13746  ghmmhmb  13807  opprrngbg  14057  opprringbg  14059  issubrng2  14190  issubrg2  14221  eltg3  14747  bastop  14765  cnptoprest  14929  cos11  15543  zabsle1  15694  lgsabs1  15734  lgsquadlem2  15773  bj-om  16383