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  2097  euan  2110  exmoeudc  2117  nebidc  2456  cgsexg  2807  cgsex2g  2808  cgsex4g  2809  elab3gf  2923  abidnf  2941  elsn2g  3666  difsn  3770  prel12  3812  dfnfc2  3868  intmin4  3913  dfiin2g  3960  elpw2g  4201  ordsucg  4551  ssrel  4764  ssrel2  4766  ssrelrel  4776  releldmb  4916  relelrnb  4917  cnveqb  5139  dmsnopg  5155  relcnvtr  5203  relcnvexb  5223  f1ocnvb  5538  ffvresb  5745  fconstfvm  5804  fnoprabg  6048  dfsmo2  6375  nntri2  6582  nntri1  6584  en1bg  6894  pw2f1odclem  6933  fieq0  7080  djulclb  7159  ismkvnex  7259  nngt1ne1  9073  znegclb  9407  iccneg  10113  fzsn  10190  fz1sbc  10220  fzofzp1b  10359  ceilqidz  10463  flqeqceilz  10465  reim0b  11206  rexanre  11564  dvdsext  12199  zob  12235  pc11  12687  pcz  12688  gsumval2  13262  issubg2m  13558  issubg4m  13562  ghmmhmb  13623  opprrngbg  13873  opprringbg  13875  issubrng2  14005  issubrg2  14036  eltg3  14562  bastop  14580  cnptoprest  14744  cos11  15358  zabsle1  15509  lgsabs1  15549  lgsquadlem2  15588  bj-om  15910