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  3771  dfnfc2  3827  intmin4  3872  dfiin2g  3919  elpw2g  4156  ordsucg  4501  ssrel  4714  ssrel2  4716  ssrelrel  4726  releldmb  4864  relelrnb  4865  cnveqb  5084  dmsnopg  5100  relcnvtr  5148  relcnvexb  5168  f1ocnvb  5475  ffvresb  5679  fconstfvm  5734  fnoprabg  5975  dfsmo2  6287  nntri2  6494  nntri1  6496  en1bg  6799  fieq0  6974  djulclb  7053  ismkvnex  7152  nngt1ne1  8953  znegclb  9285  iccneg  9988  fzsn  10065  fz1sbc  10095  fzofzp1b  10227  ceilqidz  10315  flqeqceilz  10317  reim0b  10870  rexanre  11228  dvdsext  11860  zob  11895  pc11  12329  pcz  12330  issubg2m  13047  issubg4m  13051  opprringbg  13248  issubrg2  13360  eltg3  13527  bastop  13545  cnptoprest  13709  cos11  14244  zabsle1  14370  lgsabs1  14410  bj-om  14659