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  6562  nntri2  6771  nntri1  6773  en1bg  7091  pw2f1odclem  7138  fieq0  7315  djulclb  7401  ismkvnex  7501  nngt1ne1  9348  znegclb  9688  iccneg  10408  fzsn  10489  fz1sbc  10520  fzofzp1b  10663  ceilqidz  10774  flqeqceilz  10776  reim0b  11649  rexanre  12009  dvdsext  12647  zob  12683  pc11  13139  pcz  13140  gzsumval2  13773  issubg2m  14051  issubg4m  14055  ghmmhmb  14116  opprrngbg  14492  opprringbg  14494  issubrng2  14627  issubrg2  14658  aprlring  14709  eltg3  15283  bastop  15301  cnptoprest  15465  cos11  16081  zabsle1  16323  lgsabs1  16363  lgsquadlem2  16402  issubgr2  16704  uhgrissubgr  16707  clwwlknun  16887  bj-om  17168  stnot  17244  qdiff  17305