Theorem impbid2 228

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimt  362  bimsc1  855  biorf  947  pm4.72  962  19.38a  1860  19.38b  1861  ax13b  2052  19.3t  2236  cgsexg  3498  cgsex2g  3499  cgsex4g  3500  elab3gf  3643  elab3g  3644  abidnf  3665  reuan  3849  sscon34b  4256  r19.3rzv  4457  elsn2g  4623  eqoreldif  4644  difsn  4758  elpreqprb  4826  dfnfc2  4887  intmin4  4935  elpw2g  5289  ssrel  5755  ssrel2  5757  ssrelrel  5768  dmopab2rex  5893  releldmb  5922  relelrnb  5923  cnveqb  6183  dmsnopg  6200  relcnvtrg  6254  elsnxp  6278  onelssex  6395  ord0eln0  6402  f1ocnvb  6820  eqfnun  7018  ffvresb  7107  isof1oopb  7309  soisores  7311  riotaclb  7394  fnoprabg  7519  difex2  7743  dfwe2  7757  ordpwsuc  7795  ordunisuc2  7824  limsssuc  7830  dfom2  7848  relcnvexb  7907  dfsmo2  8318  ord1eln01  8465  ord2eln012  8466  omord  8537  nneob  8626  fsetcdmex  8844  pw2f1olem  9053  pwssfi  9145  sucdom  9188  1sdom  9199  fundmfibi  9279  f1dmvrnfibi  9284  fieq0  9367  hartogslem1  9490  rankr1ag  9760  rankeq0b  9818  fidomtri  9951  fidomtri2  9952  pr2ne  9961  isfin2-2  10276  enfin2i  10278  isfin3-2  10324  isf34lem6  10337  isfin1-2  10342  isfin1-3  10343  isfin7-2  10353  axgroth6  10786  ltsonq  10927  ltexnq  10933  znegclb  12608  rpneg  13027  nltpnft  13167  ngtmnft  13169  xrrebnd  13171  qextlt  13206  qextle  13207  iccneg  13476  fzsn  13571  fz1sbc  13605  fzdif1  13610  fzofzp1b  13771  ceilidz  13862  fleqceilz  13864  hashclb  14371  hashnncl  14379  hashfun  14450  reim0b  15146  rexanre  15374  rexuzre  15380  lo1resb  15591  o1resb  15593  dvdsext  16355  zob  16393  ncoprmgcdne1b  16684  pceq0  16907  pc11  16916  pcz  16917  ramtcl  17046  cshwsiun  17135  oduposb  18359  pospo  18375  cnvpsb  18611  tsrlemax  18618  issubg2  19183  issubg4  19187  eqg0subg  19237  ghmmhmb  19267  pmtrmvd  19496  mndodcong  19582  issubrng2  20608  issubrg2  20642  ring2idlqusb  21380  lpigen  21405  cyggic  21624  ip2eq  21705  maducoeval2  22700  eltg3  23022  bastop  23041  0top  23043  iscld3  23124  isclo2  23148  cnprest  23349  dfconn2  23479  comppfsc  23592  cmphaushmeo  23860  reghaus  23885  nrmhaus  23886  fbun  23900  fsubbas  23927  ufileu  23979  uffix  23981  txflf  24066  fclsrest  24084  flimfnfcls  24088  ptcmplem2  24113  tgpt1  24178  tgpt0  24179  isngp2  24657  nrgdomn  24731  nmhmcn  25182  iscmet3  25355  limcflf  25943  ply1nzb  26183  coe11  26313  dgreq0  26325  eldmgm  27086  sqf11  27203  sqff1o  27246  zabsle1  27360  lgsabs1  27400  lgsquadlem2  27445  madebday  27993  oldbday  27994  leslss  28002  oldfib  28470  z12negsclb  28574  bdayfin  28580  issubgr2  29473  uhgrissubgr  29476  usgrfilem  29528  uvtxnbgrb  29602  nbusgrvtxm1uvtx  29606  cusgrfilem3  29658  vdiscusgr  29732  wwlksn0s  30061  clwwlknon1loop  30300  clwwlknun  30314  nmobndi  30978  hmopadj2  32144  mdslle1i  32520  mdslle2i  32521  relfi  32802  ssrelf  32817  prodindf  33040  bnj1173  35297  r1filim  35400  revwlkb  35476  resconn  35596  cvmsval  35616  fmlafvel  35735  dmopab3rexdif  35755  elmrsubrn  35870  funsseq  36118  brcolinear  36409  outsideofeu  36481  lineunray  36497  nn0prpw  36683  ttcsnexbig  36881  bj-nfimexal  37081  bj-spvw  37107  bj-sngltag  37468  bj-elpwg  37537  bj-elsn0  37647  bj-opelid  37648  bj-opelidres  37653  bj-ideqg1  37656  bj-imdirval3  37676  bj-inftyexpiinj  37701  qdiff  37819  poimirlem26  38145  poimirlem27  38146  heicant  38154  cover2  38214  isbndx  38281  isbnd2  38282  equivbnd2  38291  prdsbnd2  38294  elghomlem2OLD  38385  isdrngo3  38458  riotaclbgBAD  39578  lssatle  39639  opcon3b  39820  cdlemk33N  41533  cdlemk34  41534  ioin9i8  42824  eu6w  43258  wepwsolem  43619  onsupmaxb  43816  rp-fakeimass  44088  iscard5  44112  cnvssb  44162  intimag  44232  ntrneiiso  44667  pm11.71  44973  pm14.122b  44999  pm14.123b  45002  iotavalb  45006  relwf  45543  elixpconstg  45667  eliuniin  45677  eliuniin2  45698  climreeq  46189  f1cof1b  47671  rexrsb  47694  afv0nbfvbi  47745  dfafn5b  47755  elfz2z  47909  zeo2ALTV  48293  fpprwpprb  48362  dfsclnbgr6  48480  nnlog2ge0lt1  49188  oppccatb  49637