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  1841  19.38b  1842  ax13b  2033  19.3t  2206  cgsexg  3483  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  elab3gf  3637  elab3g  3638  abidnf  3658  reuan  3844  sscon34b  4254  r19.3rzv  4454  elsn2g  4619  eqoreldif  4640  difsn  4752  elpreqprb  4822  dfnfc2  4883  intmin4  4930  dfiin2g  4984  elpw2g  5276  ssrel  5730  ssrel2  5732  ssrelrel  5743  dmopab2rex  5864  releldmb  5893  relelrnb  5894  cnveqb  6152  dmsnopg  6169  relcnvtrg  6223  elsnxp  6247  onelssex  6364  ord0eln0  6371  f1ocnvb  6785  eqfnun  6980  ffvresb  7068  isof1oopb  7269  soisores  7271  riotaclb  7354  fnoprabg  7479  difex2  7703  dfwe2  7717  ordpwsuc  7755  ordunisuc2  7784  limsssuc  7790  dfom2  7808  relcnvexb  7866  dfsmo2  8277  ord1eln01  8421  ord2eln012  8422  omord  8493  nneob  8582  fsetcdmex  8798  pw2f1olem  9007  pwssfi  9099  sucdom  9142  1sdom  9153  fundmfibi  9234  f1dmvrnfibi  9239  fieq0  9322  hartogslem1  9445  rankr1ag  9712  rankeq0b  9770  fidomtri  9903  fidomtri2  9904  pr2ne  9913  isfin2-2  10227  enfin2i  10229  isfin3-2  10275  isf34lem6  10288  isfin1-2  10293  isfin1-3  10294  isfin7-2  10304  axgroth6  10737  ltsonq  10878  ltexnq  10884  znegclb  12526  rpneg  12937  nltpnft  13077  ngtmnft  13079  xrrebnd  13081  qextlt  13116  qextle  13117  iccneg  13386  fzsn  13480  fz1sbc  13514  fzdif1  13519  fzofzp1b  13679  ceilidz  13770  fleqceilz  13772  hashclb  14279  hashnncl  14287  hashfun  14358  reim0b  15040  rexanre  15268  rexuzre  15274  lo1resb  15485  o1resb  15487  dvdsext  16246  zob  16284  ncoprmgcdne1b  16575  pceq0  16797  pc11  16806  pcz  16807  ramtcl  16936  cshwsiun  17025  oduposb  18248  pospo  18264  cnvpsb  18500  tsrlemax  18507  issubg2  19069  issubg4  19073  eqg0subg  19123  ghmmhmb  19154  pmtrmvd  19383  mndodcong  19469  issubrng2  20489  issubrg2  20523  ring2idlqusb  21263  lpigen  21288  cyggic  21525  ip2eq  21606  maducoeval2  22582  eltg3  22904  bastop  22923  0top  22925  iscld3  23006  isclo2  23030  cnprest  23231  dfconn2  23361  comppfsc  23474  cmphaushmeo  23742  reghaus  23767  nrmhaus  23768  fbun  23782  fsubbas  23809  ufileu  23861  uffix  23863  txflf  23948  fclsrest  23966  flimfnfcls  23970  ptcmplem2  23995  tgpt1  24060  tgpt0  24061  isngp2  24539  nrgdomn  24613  nmhmcn  25074  iscmet3  25247  limcflf  25836  ply1nzb  26082  coe11  26212  dgreq0  26225  eldmgm  26986  sqf11  27103  sqff1o  27146  zabsle1  27261  lgsabs1  27301  lgsquadlem2  27346  madebday  27872  oldbday  27873  slelss  27881  oldfib  28335  zs12negsclb  28430  issubgr2  29294  uhgrissubgr  29297  usgrfilem  29349  uvtxnbgrb  29423  nbusgrvtxm1uvtx  29427  cusgrfilem3  29480  vdiscusgr  29554  wwlksn0s  29883  clwwlknon1loop  30122  clwwlknun  30136  nmobndi  30799  hmopadj2  31965  mdslle1i  32341  mdslle2i  32342  relfi  32626  ssrelf  32642  prodindf  32893  bnj1173  35107  r1filim  35209  revwlkb  35269  resconn  35389  cvmsval  35409  fmlafvel  35528  dmopab3rexdif  35548  elmrsubrn  35663  funsseq  35911  brcolinear  36202  outsideofeu  36274  lineunray  36290  nn0prpw  36466  bj-nfimexal  36769  bj-sngltag  37127  bj-elpwg  37196  bj-elsn0  37299  bj-opelid  37300  bj-opelidres  37305  bj-ideqg1  37308  bj-imdirval3  37328  bj-inftyexpiinj  37353  poimirlem26  37786  poimirlem27  37787  heicant  37795  cover2  37855  isbndx  37922  isbnd2  37923  equivbnd2  37932  prdsbnd2  37935  elghomlem2OLD  38026  isdrngo3  38099  riotaclbgBAD  39153  lssatle  39214  opcon3b  39395  cdlemk33N  41108  cdlemk34  41109  ioin9i8  42400  eu6w  42861  wepwsolem  43226  onsupmaxb  43423  rp-fakeimass  43695  iscard5  43719  cnvssb  43769  intimag  43839  ntrneiiso  44274  pm11.71  44580  pm14.122b  44606  pm14.123b  44609  iotavalb  44613  relwf  45150  elixpconstg  45275  eliuniin  45285  eliuniin2  45306  climreeq  45801  f1cof1b  47265  rexrsb  47288  afv0nbfvbi  47339  dfafn5b  47349  elfz2z  47503  zeo2ALTV  47859  fpprwpprb  47928  dfsclnbgr6  48046  nnlog2ge0lt1  48754  oppccatb  49203