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  687  biorf  746  biorfi  748  pm4.72  829  con34bdc  873  notnotbdc  874  dfandc  886  imanst  890  dfordc  894  dfor2dc  897  pm4.79dc  905  orimdidc  908  pm5.54dc  920  pm5.62dc  948  bimsc1  966  modc  2099  euan  2112  exmoeudc  2119  nebidc  2458  cgsexg  2812  cgsex2g  2813  cgsex4g  2814  elab3gf  2930  abidnf  2948  elsn2g  3676  difsn  3781  prel12  3825  dfnfc2  3882  intmin4  3927  dfiin2g  3974  elpw2g  4216  ordsucg  4568  ssrel  4781  ssrel2  4783  ssrelrel  4793  releldmb  4934  relelrnb  4935  cnveqb  5157  dmsnopg  5173  relcnvtr  5221  relcnvexb  5241  f1ocnvb  5558  ffvresb  5766  fconstfvm  5825  fnoprabg  6069  dfsmo2  6396  nntri2  6603  nntri1  6605  en1bg  6915  pw2f1odclem  6956  fieq0  7104  djulclb  7183  ismkvnex  7283  nngt1ne1  9106  znegclb  9440  iccneg  10146  fzsn  10223  fz1sbc  10253  fzofzp1b  10394  ceilqidz  10498  flqeqceilz  10500  reim0b  11288  rexanre  11646  dvdsext  12281  zob  12317  pc11  12769  pcz  12770  gsumval2  13344  issubg2m  13640  issubg4m  13644  ghmmhmb  13705  opprrngbg  13955  opprringbg  13957  issubrng2  14087  issubrg2  14118  eltg3  14644  bastop  14662  cnptoprest  14826  cos11  15440  zabsle1  15591  lgsabs1  15631  lgsquadlem2  15670  bj-om  16072