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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimt  241  mtt  696  biorf  756  biorfi  758  pm4.72  839  con34bdc  883  notnotbdc  884  dfandc  896  imanst  900  dfordc  904  dfor2dc  907  pm4.79dc  915  orimdidc  918  pm5.54dc  930  pm5.62dc  958  bimsc1  976  dfifp2dc  994  modc  2130  euan  2143  exmoeudc  2150  nebidc  2500  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  elab3gf  2976  abidnf  2994  elsn2g  3742  difsn  3852  prel12  3896  dfnfc2  3953  intmin4  3998  dfiin2g  4045  elpw2g  4292  ordsucg  4649  ssrel  4863  ssrel2  4865  ssrelrel  4875  releldmb  5019  relelrnb  5020  cnveqb  5243  dmsnopg  5259  relcnvtr  5307  relcnvexb  5327  f1ocnvb  5653  ffvresb  5871  fconstfvm  5933  fnoprabg  6189  dfsmo2  6558  nntri2  6767  nntri1  6769  en1bg  7087  pw2f1odclem  7134  fieq0  7310  djulclb  7395  ismkvnex  7495  nngt1ne1  9341  znegclb  9681  iccneg  10401  fzsn  10482  fz1sbc  10513  fzofzp1b  10656  ceilqidz  10766  flqeqceilz  10768  reim0b  11641  rexanre  12001  dvdsext  12638  zob  12674  pc11  13130  pcz  13131  gzsumval2  13763  issubg2m  14041  issubg4m  14045  ghmmhmb  14106  opprrngbg  14432  opprringbg  14434  issubrng2  14567  issubrg2  14598  aprlring  14649  eltg3  15207  bastop  15225  cnptoprest  15389  cos11  16004  zabsle1  16216  lgsabs1  16256  lgsquadlem2  16295  issubgr2  16597  uhgrissubgr  16600  clwwlknun  16780  bj-om  17061  stnot  17137  qdiff  17196