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	⊢ (𝜓 → 𝜒)
impbid2.2	⊢ (𝜑 → (𝜒 → 𝜓))

Assertion

Ref	Expression
impbid2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
2		impbid2.1	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	impbid1 142	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 141	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

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  2098  euan  2111  exmoeudc  2118  nebidc  2457  cgsexg  2809  cgsex2g  2810  cgsex4g  2811  elab3gf  2927  abidnf  2945  elsn2g  3671  difsn  3776  prel12  3820  dfnfc2  3877  intmin4  3922  dfiin2g  3969  elpw2g  4211  ordsucg  4563  ssrel  4776  ssrel2  4778  ssrelrel  4788  releldmb  4929  relelrnb  4930  cnveqb  5152  dmsnopg  5168  relcnvtr  5216  relcnvexb  5236  f1ocnvb  5553  ffvresb  5761  fconstfvm  5820  fnoprabg  6064  dfsmo2  6391  nntri2  6598  nntri1  6600  en1bg  6910  pw2f1odclem  6951  fieq0  7099  djulclb  7178  ismkvnex  7278  nngt1ne1  9101  znegclb  9435  iccneg  10141  fzsn  10218  fz1sbc  10248  fzofzp1b  10389  ceilqidz  10493  flqeqceilz  10495  reim0b  11258  rexanre  11616  dvdsext  12251  zob  12287  pc11  12739  pcz  12740  gsumval2  13314  issubg2m  13610  issubg4m  13614  ghmmhmb  13675  opprrngbg  13925  opprringbg  13927  issubrng2  14057  issubrg2  14088  eltg3  14614  bastop  14632  cnptoprest  14796  cos11  15410  zabsle1  15561  lgsabs1  15601  lgsquadlem2  15640  bj-om  16042