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  686  biorf  745  biorfi  747  pm4.72  828  con34bdc  872  notnotbdc  873  dfandc  885  imanst  889  dfordc  893  dfor2dc  896  pm4.79dc  904  orimdidc  907  pm5.54dc  919  pm5.62dc  947  bimsc1  965  modc  2085  euan  2098  exmoeudc  2105  nebidc  2444  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  elab3gf  2910  abidnf  2928  elsn2g  3651  difsn  3755  prel12  3797  dfnfc2  3853  intmin4  3898  dfiin2g  3945  elpw2g  4185  ordsucg  4534  ssrel  4747  ssrel2  4749  ssrelrel  4759  releldmb  4899  relelrnb  4900  cnveqb  5121  dmsnopg  5137  relcnvtr  5185  relcnvexb  5205  f1ocnvb  5514  ffvresb  5721  fconstfvm  5776  fnoprabg  6019  dfsmo2  6340  nntri2  6547  nntri1  6549  en1bg  6854  pw2f1odclem  6890  fieq0  7035  djulclb  7114  ismkvnex  7214  nngt1ne1  9017  znegclb  9350  iccneg  10055  fzsn  10132  fz1sbc  10162  fzofzp1b  10295  ceilqidz  10387  flqeqceilz  10389  reim0b  11006  rexanre  11364  dvdsext  11997  zob  12032  pc11  12469  pcz  12470  gsumval2  12980  issubg2m  13259  issubg4m  13263  ghmmhmb  13324  opprrngbg  13574  opprringbg  13576  issubrng2  13706  issubrg2  13737  eltg3  14225  bastop  14243  cnptoprest  14407  cos11  14988  zabsle1  15115  lgsabs1  15155  bj-om  15429