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  689  biorf  749  biorfi  751  pm4.72  832  con34bdc  876  notnotbdc  877  dfandc  889  imanst  893  dfordc  897  dfor2dc  900  pm4.79dc  908  orimdidc  911  pm5.54dc  923  pm5.62dc  951  bimsc1  969  dfifp2dc  987  modc  2121  euan  2134  exmoeudc  2141  nebidc  2480  cgsexg  2836  cgsex2g  2837  cgsex4g  2838  elab3gf  2954  abidnf  2972  elsn2g  3700  difsn  3808  prel12  3852  dfnfc2  3909  intmin4  3954  dfiin2g  4001  elpw2g  4244  ordsucg  4598  ssrel  4812  ssrel2  4814  ssrelrel  4824  releldmb  4967  relelrnb  4968  cnveqb  5190  dmsnopg  5206  relcnvtr  5254  relcnvexb  5274  f1ocnvb  5594  ffvresb  5806  fconstfvm  5867  fnoprabg  6117  dfsmo2  6448  nntri2  6657  nntri1  6659  en1bg  6969  pw2f1odclem  7015  fieq0  7166  djulclb  7245  ismkvnex  7345  nngt1ne1  9168  znegclb  9502  iccneg  10214  fzsn  10291  fz1sbc  10321  fzofzp1b  10463  ceilqidz  10568  flqeqceilz  10570  reim0b  11413  rexanre  11771  dvdsext  12406  zob  12442  pc11  12894  pcz  12895  gsumval2  13470  issubg2m  13766  issubg4m  13770  ghmmhmb  13831  opprrngbg  14081  opprringbg  14083  issubrng2  14214  issubrg2  14245  eltg3  14771  bastop  14789  cnptoprest  14953  cos11  15567  zabsle1  15718  lgsabs1  15758  lgsquadlem2  15797  clwwlknun  16236  bj-om  16468