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  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  3738  difsn  3847  prel12  3891  dfnfc2  3948  intmin4  3993  dfiin2g  4040  elpw2g  4287  ordsucg  4644  ssrel  4858  ssrel2  4860  ssrelrel  4870  releldmb  5014  relelrnb  5015  cnveqb  5238  dmsnopg  5254  relcnvtr  5302  relcnvexb  5322  f1ocnvb  5648  ffvresb  5862  fconstfvm  5924  fnoprabg  6179  dfsmo2  6548  nntri2  6757  nntri1  6759  en1bg  7077  pw2f1odclem  7124  fieq0  7300  djulclb  7385  ismkvnex  7485  nngt1ne1  9318  znegclb  9656  iccneg  10370  fzsn  10450  fz1sbc  10481  fzofzp1b  10624  ceilqidz  10731  flqeqceilz  10733  reim0b  11605  rexanre  11964  dvdsext  12600  zob  12636  pc11  13088  pcz  13089  gzsumval2  13691  issubg2m  13969  issubg4m  13973  ghmmhmb  14034  opprrngbg  14356  opprringbg  14358  issubrng2  14491  issubrg2  14522  aprlring  14573  eltg3  15081  bastop  15099  cnptoprest  15263  cos11  15877  zabsle1  16032  lgsabs1  16072  lgsquadlem2  16111  issubgr2  16413  uhgrissubgr  16416  clwwlknun  16596  bj-om  16877  qdiff  17003