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

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimt  241  mtt  692  biorf  752  biorfi  754  pm4.72  835  con34bdc  879  notnotbdc  880  dfandc  892  imanst  896  dfordc  900  dfor2dc  903  pm4.79dc  911  orimdidc  914  pm5.54dc  926  pm5.62dc  954  bimsc1  972  dfifp2dc  990  modc  2126  euan  2139  exmoeudc  2146  nebidc  2494  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  elab3gf  2969  abidnf  2987  elsn2g  3724  difsn  3833  prel12  3877  dfnfc2  3934  intmin4  3979  dfiin2g  4026  elpw2g  4270  ordsucg  4626  ssrel  4840  ssrel2  4842  ssrelrel  4852  releldmb  4996  relelrnb  4997  cnveqb  5220  dmsnopg  5236  relcnvtr  5284  relcnvexb  5304  f1ocnvb  5630  ffvresb  5842  fconstfvm  5904  fnoprabg  6156  dfsmo2  6520  nntri2  6729  nntri1  6731  en1bg  7042  pw2f1odclem  7089  fieq0  7265  djulclb  7348  ismkvnex  7448  nngt1ne1  9274  znegclb  9612  iccneg  10325  fzsn  10403  fz1sbc  10434  fzofzp1b  10577  ceilqidz  10682  flqeqceilz  10684  reim0b  11551  rexanre  11909  dvdsext  12545  zob  12581  pc11  13033  pcz  13034  gsumval2  13627  issubg2m  13923  issubg4m  13927  ghmmhmb  13988  opprrngbg  14239  opprringbg  14241  issubrng2  14372  issubrg2  14403  aprlring  14451  eltg3  14939  bastop  14957  cnptoprest  15121  cos11  15735  zabsle1  15889  lgsabs1  15929  lgsquadlem2  15968  issubgr2  16270  uhgrissubgr  16273  clwwlknun  16453  bj-om  16724  qdiff  16850