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  2088  euan  2101  exmoeudc  2108  nebidc  2447  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  elab3gf  2914  abidnf  2932  elsn2g  3656  difsn  3760  prel12  3802  dfnfc2  3858  intmin4  3903  dfiin2g  3950  elpw2g  4190  ordsucg  4539  ssrel  4752  ssrel2  4754  ssrelrel  4764  releldmb  4904  relelrnb  4905  cnveqb  5126  dmsnopg  5142  relcnvtr  5190  relcnvexb  5210  f1ocnvb  5521  ffvresb  5728  fconstfvm  5783  fnoprabg  6027  dfsmo2  6354  nntri2  6561  nntri1  6563  en1bg  6868  pw2f1odclem  6904  fieq0  7051  djulclb  7130  ismkvnex  7230  nngt1ne1  9044  znegclb  9378  iccneg  10083  fzsn  10160  fz1sbc  10190  fzofzp1b  10323  ceilqidz  10427  flqeqceilz  10429  reim0b  11046  rexanre  11404  dvdsext  12039  zob  12075  pc11  12527  pcz  12528  gsumval2  13101  issubg2m  13397  issubg4m  13401  ghmmhmb  13462  opprrngbg  13712  opprringbg  13714  issubrng2  13844  issubrg2  13875  eltg3  14401  bastop  14419  cnptoprest  14583  cos11  15197  zabsle1  15348  lgsabs1  15388  lgsquadlem2  15427  bj-om  15691