Theorem impbid2 226

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimt  360  bimsc1  844  biorf  936  pm4.72  951  19.38a  1840  19.38b  1841  ax13b  2032  19.3t  2202  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  elab3gf  3640  elab3g  3641  abidnf  3662  reuan  3848  sscon34b  4255  elsn2g  4616  eqoreldif  4637  difsn  4749  elpreqprb  4819  dfnfc2  4880  intmin4  4927  dfiin2g  4981  elpw2g  5272  ssrel  5726  ssrel2  5728  ssrelrel  5739  dmopab2rex  5860  releldmb  5888  relelrnb  5889  cnveqb  6145  dmsnopg  6162  relcnvtrg  6215  elsnxp  6239  onelssex  6356  ord0eln0  6363  f1ocnvb  6777  eqfnun  6971  ffvresb  7059  isof1oopb  7262  soisores  7264  riotaclb  7347  fnoprabg  7472  difex2  7696  dfwe2  7710  ordpwsuc  7748  ordunisuc2  7777  limsssuc  7783  dfom2  7801  relcnvexb  7859  dfsmo2  8270  ord1eln01  8414  ord2eln012  8415  omord  8486  nneob  8574  fsetcdmex  8790  pw2f1olem  8998  pwssfi  9091  sucdom  9133  1sdom  9144  fundmfibi  9226  f1dmvrnfibi  9231  fieq0  9311  hartogslem1  9434  rankr1ag  9698  rankeq0b  9756  fidomtri  9889  fidomtri2  9890  pr2ne  9899  isfin2-2  10213  enfin2i  10215  isfin3-2  10261  isf34lem6  10274  isfin1-2  10279  isfin1-3  10280  isfin7-2  10290  axgroth6  10722  ltsonq  10863  ltexnq  10869  znegclb  12512  rpneg  12927  nltpnft  13066  ngtmnft  13068  xrrebnd  13070  qextlt  13105  qextle  13106  iccneg  13375  fzsn  13469  fz1sbc  13503  fzdif1  13508  fzofzp1b  13668  ceilidz  13756  fleqceilz  13758  hashclb  14265  hashnncl  14273  hashfun  14344  reim0b  15026  rexanre  15254  rexuzre  15260  lo1resb  15471  o1resb  15473  dvdsext  16232  zob  16270  ncoprmgcdne1b  16561  pceq0  16783  pc11  16792  pcz  16793  ramtcl  16922  cshwsiun  17011  oduposb  18233  pospo  18249  cnvpsb  18485  tsrlemax  18492  issubg2  19020  issubg4  19024  eqg0subg  19075  ghmmhmb  19106  pmtrmvd  19335  mndodcong  19421  issubrng2  20443  issubrg2  20477  ring2idlqusb  21217  lpigen  21242  cyggic  21479  ip2eq  21560  maducoeval2  22525  eltg3  22847  bastop  22866  0top  22868  iscld3  22949  isclo2  22973  cnprest  23174  dfconn2  23304  comppfsc  23417  cmphaushmeo  23685  reghaus  23710  nrmhaus  23711  fbun  23725  fsubbas  23752  ufileu  23804  uffix  23806  txflf  23891  fclsrest  23909  flimfnfcls  23913  ptcmplem2  23938  tgpt1  24003  tgpt0  24004  isngp2  24483  nrgdomn  24557  nmhmcn  25018  iscmet3  25191  limcflf  25780  ply1nzb  26026  coe11  26156  dgreq0  26169  eldmgm  26930  sqf11  27047  sqff1o  27090  zabsle1  27205  lgsabs1  27245  lgsquadlem2  27290  madebday  27814  oldbday  27815  slelss  27823  zs12negsclb  28358  issubgr2  29217  uhgrissubgr  29220  usgrfilem  29272  uvtxnbgrb  29346  nbusgrvtxm1uvtx  29350  cusgrfilem3  29403  vdiscusgr  29477  wwlksn0s  29806  clwwlknon1loop  30042  clwwlknun  30056  nmobndi  30719  hmopadj2  31885  mdslle1i  32261  mdslle2i  32262  relfi  32546  ssrelf  32560  prodindf  32807  bnj1173  34975  revwlkb  35109  resconn  35229  cvmsval  35249  fmlafvel  35368  dmopab3rexdif  35388  elmrsubrn  35503  funsseq  35751  brcolinear  36043  outsideofeu  36115  lineunray  36131  nn0prpw  36307  bj-nfimexal  36610  bj-sngltag  36967  bj-elpwg  37036  bj-elsn0  37139  bj-opelid  37140  bj-opelidres  37145  bj-ideqg1  37148  bj-imdirval3  37168  bj-inftyexpiinj  37193  wl-ax11-lem2  37570  poimirlem26  37636  poimirlem27  37637  heicant  37645  cover2  37705  isbndx  37772  isbnd2  37773  equivbnd2  37782  prdsbnd2  37785  elghomlem2OLD  37876  isdrngo3  37949  riotaclbgBAD  38943  lssatle  39004  opcon3b  39185  cdlemk33N  40898  cdlemk34  40899  ioin9i8  42190  eu6w  42659  wepwsolem  43025  onsupmaxb  43222  rp-fakeimass  43495  iscard5  43519  cnvssb  43569  intimag  43639  ntrneiiso  44074  pm11.71  44380  pm14.122b  44406  pm14.123b  44409  iotavalb  44413  relwf  44951  elixpconstg  45077  eliuniin  45087  eliuniin2  45108  climreeq  45604  f1cof1b  47071  rexrsb  47094  afv0nbfvbi  47145  dfafn5b  47155  elfz2z  47309  zeo2ALTV  47665  fpprwpprb  47734  dfsclnbgr6  47852  nnlog2ge0lt1  48561  oppccatb  49011