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  3655  difsn  3759  prel12  3801  dfnfc2  3857  intmin4  3902  dfiin2g  3949  elpw2g  4189  ordsucg  4538  ssrel  4751  ssrel2  4753  ssrelrel  4763  releldmb  4903  relelrnb  4904  cnveqb  5125  dmsnopg  5141  relcnvtr  5189  relcnvexb  5209  f1ocnvb  5518  ffvresb  5725  fconstfvm  5780  fnoprabg  6023  dfsmo2  6345  nntri2  6552  nntri1  6554  en1bg  6859  pw2f1odclem  6895  fieq0  7042  djulclb  7121  ismkvnex  7221  nngt1ne1  9025  znegclb  9359  iccneg  10064  fzsn  10141  fz1sbc  10171  fzofzp1b  10304  ceilqidz  10408  flqeqceilz  10410  reim0b  11027  rexanre  11385  dvdsext  12020  zob  12056  pc11  12500  pcz  12501  gsumval2  13040  issubg2m  13319  issubg4m  13323  ghmmhmb  13384  opprrngbg  13634  opprringbg  13636  issubrng2  13766  issubrg2  13797  eltg3  14293  bastop  14311  cnptoprest  14475  cos11  15089  zabsle1  15240  lgsabs1  15280  lgsquadlem2  15319  bj-om  15583