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  4294  ordsucg  4651  ssrel  4865  ssrel2  4867  ssrelrel  4877  releldmb  5021  relelrnb  5022  cnveqb  5246  dmsnopg  5262  relcnvtr  5310  relcnvexb  5330  f1ocnvb  5656  ffvresb  5874  fconstfvm  5936  fnoprabg  6192  dfsmo2  6563  nntri2  6772  nntri1  6774  en1bg  7093  pw2f1odclem  7140  fieq0  7315  djulclb  7401  ismkvnex  7501  nngt1ne1  9348  znegclb  9686  iccneg  10407  fzsn  10488  fz1sbc  10519  fzofzp1b  10662  ceilqidz  10773  flqeqceilz  10775  reim0b  11648  rexanre  12008  dvdsext  12646  zob  12682  pc11  13138  pcz  13139  gzsumval2  13772  issubg2m  14050  issubg4m  14054  ghmmhmb  14115  opprrngbg  14491  opprringbg  14493  issubrng2  14626  issubrg2  14657  aprlring  14708  eltg3  15300  bastop  15318  cnptoprest  15482  cos11  16098  zabsle1  16340  lgsabs1  16380  lgsquadlem2  16419  issubgr2  16721  uhgrissubgr  16724  clwwlknun  16904  bj-om  17185  stnot  17261  qdiff  17322