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  686  biorf  745  biorfi  747  pm4.72  828  con34bdc  872  notnotbdc  873  dfandc  885  imanst  889  dfordc  893  dfor2dc  896  pm4.79dc  904  orimdidc  907  pm5.54dc  919  pm5.62dc  947  bimsc1  965  modc  2088  euan  2101  exmoeudc  2108  nebidc  2447  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  elab3gf  2914  abidnf  2932  elsn2g  3656  difsn  3760  prel12  3802  dfnfc2  3858  intmin4  3903  dfiin2g  3950  elpw2g  4190  ordsucg  4539  ssrel  4752  ssrel2  4754  ssrelrel  4764  releldmb  4904  relelrnb  4905  cnveqb  5126  dmsnopg  5142  relcnvtr  5190  relcnvexb  5210  f1ocnvb  5519  ffvresb  5726  fconstfvm  5781  fnoprabg  6024  dfsmo2  6346  nntri2  6553  nntri1  6555  en1bg  6860  pw2f1odclem  6896  fieq0  7043  djulclb  7122  ismkvnex  7222  nngt1ne1  9027  znegclb  9361  iccneg  10066  fzsn  10143  fz1sbc  10173  fzofzp1b  10306  ceilqidz  10410  flqeqceilz  10412  reim0b  11029  rexanre  11387  dvdsext  12022  zob  12058  pc11  12510  pcz  12511  gsumval2  13050  issubg2m  13329  issubg4m  13333  ghmmhmb  13394  opprrngbg  13644  opprringbg  13646  issubrng2  13776  issubrg2  13807  eltg3  14303  bastop  14321  cnptoprest  14485  cos11  15099  zabsle1  15250  lgsabs1  15290  lgsquadlem2  15329  bj-om  15593