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  685  biorf  744  biorfi  746  pm4.72  827  con34bdc  871  notnotbdc  872  dfandc  884  imanst  888  dfordc  892  dfor2dc  895  pm4.79dc  903  orimdidc  906  pm5.54dc  918  pm5.62dc  945  bimsc1  963  modc  2069  euan  2082  exmoeudc  2089  nebidc  2427  cgsexg  2772  cgsex2g  2773  cgsex4g  2774  elab3gf  2887  abidnf  2905  elsn2g  3625  difsn  3729  prel12  3770  dfnfc2  3826  intmin4  3871  dfiin2g  3918  elpw2g  4154  ordsucg  4499  ssrel  4712  ssrel2  4714  ssrelrel  4724  releldmb  4861  relelrnb  4862  cnveqb  5081  dmsnopg  5097  relcnvtr  5145  relcnvexb  5165  f1ocnvb  5472  ffvresb  5676  fconstfvm  5731  fnoprabg  5971  dfsmo2  6283  nntri2  6490  nntri1  6492  en1bg  6795  fieq0  6970  djulclb  7049  ismkvnex  7148  nngt1ne1  8948  znegclb  9280  iccneg  9983  fzsn  10059  fz1sbc  10089  fzofzp1b  10221  ceilqidz  10309  flqeqceilz  10311  reim0b  10862  rexanre  11220  dvdsext  11851  zob  11886  pc11  12320  pcz  12321  issubg2m  12975  issubg4m  12979  opprringbg  13149  eltg3  13339  bastop  13357  cnptoprest  13521  cos11  14056  zabsle1  14182  lgsabs1  14222  bj-om  14460