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  7396  ismkvnex  7496  nngt1ne1  9342  znegclb  9682  iccneg  10402  fzsn  10483  fz1sbc  10514  fzofzp1b  10657  ceilqidz  10768  flqeqceilz  10770  reim0b  11643  rexanre  12003  dvdsext  12641  zob  12677  pc11  13133  pcz  13134  gzsumval2  13767  issubg2m  14045  issubg4m  14049  ghmmhmb  14110  opprrngbg  14467  opprringbg  14469  issubrng2  14602  issubrg2  14633  aprlring  14684  eltg3  15249  bastop  15267  cnptoprest  15431  cos11  16046  zabsle1  16284  lgsabs1  16324  lgsquadlem2  16363  issubgr2  16665  uhgrissubgr  16668  clwwlknun  16848  bj-om  17129  stnot  17205  qdiff  17265