Theorem impbid2 142

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 141	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 140	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimt  240  mtt  646  biorf  699  biorfi  701  pm4.72  773  biort  775  imanst  780  con34bdc  804  notnotbdc  805  dfandc  817  dfordc  830  dfor2dc  833  pm4.79dc  848  orimdidc  851  pm5.54dc  866  pm5.62dc  892  bimsc1  910  modc  1992  euan  2005  exmoeudc  2012  nebidc  2336  cgsexg  2655  cgsex2g  2656  cgsex4g  2657  elab3gf  2766  abidnf  2784  elsn2g  3481  difsn  3580  prel12  3621  dfnfc2  3677  intmin4  3722  dfiin2g  3769  elpw2g  3998  ordsucg  4332  ssrel  4539  ssrel2  4541  ssrelrel  4551  releldmb  4685  relelrnb  4686  cnveqb  4899  dmsnopg  4915  relcnvtr  4963  relcnvexb  4983  f1ocnvb  5280  ffvresb  5475  fconstfvm  5529  fnoprabg  5760  dfsmo2  6066  nntri2  6269  nntri1  6271  en1bg  6571  djulclb  6801  nngt1ne1  8518  znegclb  8844  iccneg  9467  fzsn  9541  fz1sbc  9571  fzofzp1b  9700  ceilqidz  9784  flqeqceilz  9786  reim0b  10357  rexanre  10714  dvdsext  11195  zob  11230  eltg3  11818  bastop  11836  bj-om  12105