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  2773  cgsex2g  2774  cgsex4g  2775  elab3gf  2888  abidnf  2906  elsn2g  3626  difsn  3730  prel12  3772  dfnfc2  3828  intmin4  3873  dfiin2g  3920  elpw2g  4157  ordsucg  4502  ssrel  4715  ssrel2  4717  ssrelrel  4727  releldmb  4865  relelrnb  4866  cnveqb  5085  dmsnopg  5101  relcnvtr  5149  relcnvexb  5169  f1ocnvb  5476  ffvresb  5680  fconstfvm  5735  fnoprabg  5976  dfsmo2  6288  nntri2  6495  nntri1  6497  en1bg  6800  fieq0  6975  djulclb  7054  ismkvnex  7153  nngt1ne1  8954  znegclb  9286  iccneg  9989  fzsn  10066  fz1sbc  10096  fzofzp1b  10228  ceilqidz  10316  flqeqceilz  10318  reim0b  10871  rexanre  11229  dvdsext  11861  zob  11896  pc11  12330  pcz  12331  issubg2m  13049  issubg4m  13053  opprringbg  13250  issubrg2  13362  eltg3  13560  bastop  13578  cnptoprest  13742  cos11  14277  zabsle1  14403  lgsabs1  14443  bj-om  14692