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  9339  znegclb  9677  iccneg  10391  fzsn  10472  fz1sbc  10503  fzofzp1b  10646  ceilqidz  10753  flqeqceilz  10755  reim0b  11627  rexanre  11986  dvdsext  12622  zob  12658  pc11  13110  pcz  13111  gzsumval2  13714  issubg2m  13992  issubg4m  13996  ghmmhmb  14057  opprrngbg  14383  opprringbg  14385  issubrng2  14518  issubrg2  14549  aprlring  14600  eltg3  15158  bastop  15176  cnptoprest  15340  cos11  15954  zabsle1  16118  lgsabs1  16158  lgsquadlem2  16197  issubgr2  16499  uhgrissubgr  16502  clwwlknun  16682  bj-om  16963  stnot  17039  qdiff  17098