Theorem impbid2 229

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 228	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 226	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  biimt  363  bimsc1  857  biorf  949  pm4.72  964  19.38a  1870  19.38b  1871  ax13b  2062  19.3t  2237  cgsexg  3499  cgsex2g  3500  cgsex4g  3501  elab3gf  3643  elab3g  3644  abidnf  3665  reuan  3850  sscon34b  4257  r19.3rzv  4464  elsn2g  4630  eqoreldif  4651  difsn  4766  elpreqprb  4833  dfnfc2  4894  intmin4  4942  elpw2g  5304  ssrel  5769  ssrel2  5771  ssrelrel  5782  dmopab2rex  5907  releldmb  5936  relelrnb  5937  cnveqb  6195  dmsnopg  6214  relcnvtrg  6268  elsnxp  6292  onelssex  6410  ord0eln0  6417  f1ocnvb  6834  eqfnun  7032  ffvresb  7121  isof1oopb  7323  soisores  7325  riotaclb  7408  fnoprabg  7533  difex2  7755  dfwe2  7769  ordpwsuc  7807  ordunisuc2  7836  limsssuc  7842  dfom2  7860  relcnvexb  7919  dfsmo2  8330  ord1eln01  8477  ord2eln012  8478  omord  8549  nneob  8638  fsetcdmex  8856  pw2f1olem  9065  pwssfi  9157  sucdom  9200  1sdom  9211  fundmfibi  9289  f1dmvrnfibi  9294  fieq0  9377  hartogslem1  9500  rankr1ag  9770  rankeq0b  9828  fidomtri  9975  fidomtri2  9976  pr2ne  9985  isfin2-2  10298  enfin2i  10300  isfin3-2  10346  isf34lem6  10359  isfin1-2  10364  isfin1-3  10365  isfin7-2  10375  axgroth6  10808  ltsonq  10949  ltexnq  10955  znegclb  12626  rpneg  13045  nltpnft  13185  ngtmnft  13187  xrrebnd  13189  qextlt  13224  qextle  13225  iccneg  13494  fzsn  13590  fz1sbc  13624  fzdif1  13629  fzofzp1b  13790  ceilidz  13881  fleqceilz  13883  hashclb  14390  hashnncl  14398  hashfun  14470  reim0b  15166  rexanre  15394  rexuzre  15400  lo1resb  15611  o1resb  15613  dvdsext  16374  zob  16412  ncoprmgcdne1b  16703  pceq0  16926  pc11  16935  pcz  16936  ramtcl  17065  cshwsiun  17154  oduposb  18378  pospo  18394  cnvpsb  18630  tsrlemax  18637  issubg2  19203  issubg4  19207  eqg0subg  19262  ghmmhmb  19292  pmtrmvd  19521  mndodcong  19607  issubrng2  20657  issubrg2  20691  isdrng5  20854  ring2idlqusb  21450  lpigen  21503  cyggic  21722  ip2eq  21803  maducoeval2  22797  eltg3  23119  bastop  23138  0top  23140  iscld3  23221  isclo2  23245  cnprest  23446  dfconn2  23576  comppfsc  23689  cmphaushmeo  23957  reghaus  23982  nrmhaus  23983  fbun  23997  fsubbas  24024  ufileu  24076  uffix  24078  txflf  24163  fclsrest  24181  flimfnfcls  24185  ptcmplem2  24210  tgpt1  24275  tgpt0  24276  isngp2  24754  nrgdomn  24828  nmhmcn  25279  iscmet3  25452  limcflf  26040  ply1nzb  26280  coe11  26410  dgreq0  26422  eldmgm  27186  sqf11  27303  sqff1o  27346  zabsle1  27460  lgsabs1  27500  lgsquadlem2  27545  madebday  28093  oldbday  28094  leslss  28102  oldfib  28570  z12negsclb  28674  bdayfin  28680  issubgr2  29622  uhgrissubgr  29625  usgrfilem  29677  uvtxnbgrb  29751  nbusgrvtxm1uvtx  29755  cusgrfilem3  29807  vdiscusgr  29881  wwlksn0s  30210  clwwlknon1loop  30449  clwwlknun  30463  nmobndi  31127  hmopadj2  32293  mdslle1i  32669  mdslle2i  32670  relfi  32947  ssrelf  32960  prodindf  33182  bnj1173  35390  r1filim  35498  revwlkb  35618  resconn  35738  cvmsval  35758  fmlafvel  35877  dmopab3rexdif  35897  elmrsubrn  36012  funsseq  36260  brcolinear  36551  outsideofeu  36623  lineunray  36639  nn0prpw  36854  ttcsnexbig  37052  bj-nfimexal  37251  bj-spvw  37277  bj-sngltag  37639  bj-elpwg  37708  bj-elsn0  37819  bj-opelid  37820  bj-opelidres  37825  bj-ideqg1  37828  bj-imdirval3  37848  bj-inftyexpiinj  37873  qdiff  37991  poimirlem26  38317  poimirlem27  38318  heicant  38326  cover2  38386  isbndx  38453  isbnd2  38454  equivbnd2  38463  prdsbnd2  38466  elghomlem2OLD  38557  isdrngo3  38630  riotaclbgBAD  39748  lssatle  39809  opcon3b  39990  cdlemk33N  41703  cdlemk34  41704  quadfac  42992  ioin9i8  42996  eu6w  43428  wepwsolem  43789  onsupmaxb  43986  rp-fakeimass  44258  iscard5  44282  cnvssb  44332  intimag  44402  ntrneiiso  44837  pm11.71  45127  pm14.122b  45153  pm14.123b  45156  iotavalb  45160  relwf  45696  elixpconstg  45827  eliuniin  45837  eliuniin2  45858  climreeq  46349  f1cof1b  47834  rexrsb  47857  afv0nbfvbi  47908  dfafn5b  47918  elfz2z  48072  zeo2ALTV  48456  fpprwpprb  48525  dfsclnbgr6  48643  nnlog2ge0lt1  49366  oppccatb  49814