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  845  biorf  937  pm4.72  952  19.38a  1842  19.38b  1843  ax13b  2034  19.3t  2209  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  elab3gf  3641  elab3g  3642  abidnf  3662  reuan  3848  sscon34b  4258  r19.3rzv  4458  elsn2g  4623  eqoreldif  4644  difsn  4756  elpreqprb  4826  dfnfc2  4887  intmin4  4934  dfiin2g  4988  elpw2g  5280  ssrel  5740  ssrel2  5742  ssrelrel  5753  dmopab2rex  5874  releldmb  5903  relelrnb  5904  cnveqb  6162  dmsnopg  6179  relcnvtrg  6233  elsnxp  6257  onelssex  6374  ord0eln0  6381  f1ocnvb  6795  eqfnun  6991  ffvresb  7080  isof1oopb  7281  soisores  7283  riotaclb  7366  fnoprabg  7491  difex2  7715  dfwe2  7729  ordpwsuc  7767  ordunisuc2  7796  limsssuc  7802  dfom2  7820  relcnvexb  7878  dfsmo2  8289  ord1eln01  8433  ord2eln012  8434  omord  8505  nneob  8594  fsetcdmex  8812  pw2f1olem  9021  pwssfi  9113  sucdom  9156  1sdom  9167  fundmfibi  9248  f1dmvrnfibi  9253  fieq0  9336  hartogslem1  9459  rankr1ag  9726  rankeq0b  9784  fidomtri  9917  fidomtri2  9918  pr2ne  9927  isfin2-2  10241  enfin2i  10243  isfin3-2  10289  isf34lem6  10302  isfin1-2  10307  isfin1-3  10308  isfin7-2  10318  axgroth6  10751  ltsonq  10892  ltexnq  10898  znegclb  12540  rpneg  12951  nltpnft  13091  ngtmnft  13093  xrrebnd  13095  qextlt  13130  qextle  13131  iccneg  13400  fzsn  13494  fz1sbc  13528  fzdif1  13533  fzofzp1b  13693  ceilidz  13784  fleqceilz  13786  hashclb  14293  hashnncl  14301  hashfun  14372  reim0b  15054  rexanre  15282  rexuzre  15288  lo1resb  15499  o1resb  15501  dvdsext  16260  zob  16298  ncoprmgcdne1b  16589  pceq0  16811  pc11  16820  pcz  16821  ramtcl  16950  cshwsiun  17039  oduposb  18262  pospo  18278  cnvpsb  18514  tsrlemax  18521  issubg2  19083  issubg4  19087  eqg0subg  19137  ghmmhmb  19168  pmtrmvd  19397  mndodcong  19483  issubrng2  20503  issubrg2  20537  ring2idlqusb  21277  lpigen  21302  cyggic  21539  ip2eq  21620  maducoeval2  22596  eltg3  22918  bastop  22937  0top  22939  iscld3  23020  isclo2  23044  cnprest  23245  dfconn2  23375  comppfsc  23488  cmphaushmeo  23756  reghaus  23781  nrmhaus  23782  fbun  23796  fsubbas  23823  ufileu  23875  uffix  23877  txflf  23962  fclsrest  23980  flimfnfcls  23984  ptcmplem2  24009  tgpt1  24074  tgpt0  24075  isngp2  24553  nrgdomn  24627  nmhmcn  25088  iscmet3  25261  limcflf  25850  ply1nzb  26096  coe11  26226  dgreq0  26239  eldmgm  27000  sqf11  27117  sqff1o  27160  zabsle1  27275  lgsabs1  27315  lgsquadlem2  27360  madebday  27908  oldbday  27909  leslss  27917  oldfib  28385  z12negsclb  28489  bdayfin  28495  issubgr2  29357  uhgrissubgr  29360  usgrfilem  29412  uvtxnbgrb  29486  nbusgrvtxm1uvtx  29490  cusgrfilem3  29543  vdiscusgr  29617  wwlksn0s  29946  clwwlknon1loop  30185  clwwlknun  30199  nmobndi  30863  hmopadj2  32029  mdslle1i  32405  mdslle2i  32406  relfi  32689  ssrelf  32705  prodindf  32955  bnj1173  35178  r1filim  35281  revwlkb  35342  resconn  35462  cvmsval  35482  fmlafvel  35601  dmopab3rexdif  35621  elmrsubrn  35736  funsseq  35984  brcolinear  36275  outsideofeu  36347  lineunray  36363  nn0prpw  36539  bj-nfimexal  36861  bj-spvw  36878  bj-sngltag  37231  bj-elpwg  37300  bj-elsn0  37410  bj-opelid  37411  bj-opelidres  37416  bj-ideqg1  37419  bj-imdirval3  37439  bj-inftyexpiinj  37464  poimirlem26  37897  poimirlem27  37898  heicant  37906  cover2  37966  isbndx  38033  isbnd2  38034  equivbnd2  38043  prdsbnd2  38046  elghomlem2OLD  38137  isdrngo3  38210  riotaclbgBAD  39330  lssatle  39391  opcon3b  39572  cdlemk33N  41285  cdlemk34  41286  ioin9i8  42577  eu6w  43034  wepwsolem  43399  onsupmaxb  43596  rp-fakeimass  43868  iscard5  43892  cnvssb  43942  intimag  44012  ntrneiiso  44447  pm11.71  44753  pm14.122b  44779  pm14.123b  44782  iotavalb  44786  relwf  45323  elixpconstg  45448  eliuniin  45458  eliuniin2  45479  climreeq  45973  f1cof1b  47437  rexrsb  47460  afv0nbfvbi  47511  dfafn5b  47521  elfz2z  47675  zeo2ALTV  48031  fpprwpprb  48100  dfsclnbgr6  48218  nnlog2ge0lt1  48926  oppccatb  49375