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  2123  euan  2136  exmoeudc  2143  nebidc  2483  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  elab3gf  2957  abidnf  2975  elsn2g  3706  difsn  3815  prel12  3859  dfnfc2  3916  intmin4  3961  dfiin2g  4008  elpw2g  4251  ordsucg  4606  ssrel  4820  ssrel2  4822  ssrelrel  4832  releldmb  4975  relelrnb  4976  cnveqb  5199  dmsnopg  5215  relcnvtr  5263  relcnvexb  5283  f1ocnvb  5606  ffvresb  5818  fconstfvm  5880  fnoprabg  6132  dfsmo2  6496  nntri2  6705  nntri1  6707  en1bg  7017  pw2f1odclem  7063  fieq0  7235  djulclb  7314  ismkvnex  7414  nngt1ne1  9237  znegclb  9573  iccneg  10285  fzsn  10363  fz1sbc  10393  fzofzp1b  10536  ceilqidz  10641  flqeqceilz  10643  reim0b  11502  rexanre  11860  dvdsext  12496  zob  12532  pc11  12984  pcz  12985  gsumval2  13560  issubg2m  13856  issubg4m  13860  ghmmhmb  13921  opprrngbg  14172  opprringbg  14174  issubrng2  14305  issubrg2  14336  eltg3  14868  bastop  14886  cnptoprest  15050  cos11  15664  zabsle1  15818  lgsabs1  15858  lgsquadlem2  15897  issubgr2  16199  uhgrissubgr  16202  clwwlknun  16382  bj-om  16653  qdiff  16781