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  3805  prel12  3849  dfnfc2  3906  intmin4  3951  dfiin2g  3998  elpw2g  4240  ordsucg  4594  ssrel  4807  ssrel2  4809  ssrelrel  4819  releldmb  4961  relelrnb  4962  cnveqb  5184  dmsnopg  5200  relcnvtr  5248  relcnvexb  5268  f1ocnvb  5588  ffvresb  5800  fconstfvm  5861  fnoprabg  6111  dfsmo2  6439  nntri2  6648  nntri1  6650  en1bg  6960  pw2f1odclem  7003  fieq0  7154  djulclb  7233  ismkvnex  7333  nngt1ne1  9156  znegclb  9490  iccneg  10197  fzsn  10274  fz1sbc  10304  fzofzp1b  10446  ceilqidz  10550  flqeqceilz  10552  reim0b  11388  rexanre  11746  dvdsext  12381  zob  12417  pc11  12869  pcz  12870  gsumval2  13445  issubg2m  13741  issubg4m  13745  ghmmhmb  13806  opprrngbg  14056  opprringbg  14058  issubrng2  14189  issubrg2  14220  eltg3  14746  bastop  14764  cnptoprest  14928  cos11  15542  zabsle1  15693  lgsabs1  15733  lgsquadlem2  15772  bj-om  16355