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  686  biorf  745  biorfi  747  pm4.72  828  con34bdc  872  notnotbdc  873  dfandc  885  imanst  889  dfordc  893  dfor2dc  896  pm4.79dc  904  orimdidc  907  pm5.54dc  919  pm5.62dc  947  bimsc1  965  modc  2085  euan  2098  exmoeudc  2105  nebidc  2444  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  elab3gf  2911  abidnf  2929  elsn2g  3652  difsn  3756  prel12  3798  dfnfc2  3854  intmin4  3899  dfiin2g  3946  elpw2g  4186  ordsucg  4535  ssrel  4748  ssrel2  4750  ssrelrel  4760  releldmb  4900  relelrnb  4901  cnveqb  5122  dmsnopg  5138  relcnvtr  5186  relcnvexb  5206  f1ocnvb  5515  ffvresb  5722  fconstfvm  5777  fnoprabg  6020  dfsmo2  6342  nntri2  6549  nntri1  6551  en1bg  6856  pw2f1odclem  6892  fieq0  7037  djulclb  7116  ismkvnex  7216  nngt1ne1  9019  znegclb  9353  iccneg  10058  fzsn  10135  fz1sbc  10165  fzofzp1b  10298  ceilqidz  10390  flqeqceilz  10392  reim0b  11009  rexanre  11367  dvdsext  12000  zob  12035  pc11  12472  pcz  12473  gsumval2  12983  issubg2m  13262  issubg4m  13266  ghmmhmb  13327  opprrngbg  13577  opprringbg  13579  issubrng2  13709  issubrg2  13740  eltg3  14236  bastop  14254  cnptoprest  14418  cos11  15029  zabsle1  15156  lgsabs1  15196  lgsquadlem2  15235  bj-om  15499