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  32806  bnj1173  34969  revwlkb  35103  resconn  35223  cvmsval  35243  fmlafvel  35362  dmopab3rexdif  35382  elmrsubrn  35497  funsseq  35745  brcolinear  36037  outsideofeu  36109  lineunray  36125  nn0prpw  36301  bj-nfimexal  36604  bj-sngltag  36961  bj-elpwg  37030  bj-elsn0  37133  bj-opelid  37134  bj-opelidres  37139  bj-ideqg1  37142  bj-imdirval3  37162  bj-inftyexpiinj  37187  wl-ax11-lem2  37564  poimirlem26  37630  poimirlem27  37631  heicant  37639  cover2  37699  isbndx  37766  isbnd2  37767  equivbnd2  37776  prdsbnd2  37779  elghomlem2OLD  37870  isdrngo3  37943  riotaclbgBAD  38937  lssatle  38998  opcon3b  39179  cdlemk33N  40892  cdlemk34  40893  ioin9i8  42184  eu6w  42653  wepwsolem  43019  onsupmaxb  43216  rp-fakeimass  43489  iscard5  43513  cnvssb  43563  intimag  43633  ntrneiiso  44068  pm11.71  44374  pm14.122b  44400  pm14.123b  44403  iotavalb  44407  relwf  44945  elixpconstg  45071  eliuniin  45081  eliuniin2  45102  climreeq  45598  f1cof1b  47065  rexrsb  47088  afv0nbfvbi  47139  dfafn5b  47149  elfz2z  47303  zeo2ALTV  47659  fpprwpprb  47728  dfsclnbgr6  47846  nnlog2ge0lt1  48555  oppccatb  49005