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-mp 5  ax-1 6  ax-2 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  675  biorf  734  biorfi  736  pm4.72  813  con34bdc  857  notnotbdc  858  dfandc  870  imanst  874  dfordc  878  dfor2dc  881  pm4.79dc  889  orimdidc  892  pm5.54dc  904  pm5.62dc  930  bimsc1  948  modc  2049  euan  2062  exmoeudc  2069  nebidc  2407  cgsexg  2747  cgsex2g  2748  cgsex4g  2749  elab3gf  2862  abidnf  2880  elsn2g  3594  difsn  3695  prel12  3736  dfnfc2  3792  intmin4  3837  dfiin2g  3884  elpw2g  4120  ordsucg  4464  ssrel  4677  ssrel2  4679  ssrelrel  4689  releldmb  4826  relelrnb  4827  cnveqb  5044  dmsnopg  5060  relcnvtr  5108  relcnvexb  5128  f1ocnvb  5431  ffvresb  5633  fconstfvm  5688  fnoprabg  5925  dfsmo2  6237  nntri2  6444  nntri1  6446  en1bg  6748  fieq0  6923  djulclb  7002  ismkvnex  7101  nngt1ne1  8874  znegclb  9206  iccneg  9900  fzsn  9975  fz1sbc  10005  fzofzp1b  10137  ceilqidz  10225  flqeqceilz  10227  reim0b  10774  rexanre  11132  dvdsext  11760  zob  11795  eltg3  12553  bastop  12571  cnptoprest  12735  cos11  13270  bj-om  13609