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  2835  cgsex2g  2836  cgsex4g  2837  elab3gf  2953  abidnf  2971  elsn2g  3699  difsn  3804  prel12  3848  dfnfc2  3905  intmin4  3950  dfiin2g  3997  elpw2g  4239  ordsucg  4593  ssrel  4806  ssrel2  4808  ssrelrel  4818  releldmb  4960  relelrnb  4961  cnveqb  5183  dmsnopg  5199  relcnvtr  5247  relcnvexb  5267  f1ocnvb  5585  ffvresb  5797  fconstfvm  5856  fnoprabg  6104  dfsmo2  6431  nntri2  6638  nntri1  6640  en1bg  6950  pw2f1odclem  6991  fieq0  7139  djulclb  7218  ismkvnex  7318  nngt1ne1  9141  znegclb  9475  iccneg  10181  fzsn  10258  fz1sbc  10288  fzofzp1b  10429  ceilqidz  10533  flqeqceilz  10535  reim0b  11368  rexanre  11726  dvdsext  12361  zob  12397  pc11  12849  pcz  12850  gsumval2  13425  issubg2m  13721  issubg4m  13725  ghmmhmb  13786  opprrngbg  14036  opprringbg  14038  issubrng2  14168  issubrg2  14199  eltg3  14725  bastop  14743  cnptoprest  14907  cos11  15521  zabsle1  15672  lgsabs1  15712  lgsquadlem2  15751  bj-om  16258