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  2204  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  elab3gf  3635  elab3g  3636  abidnf  3656  reuan  3842  sscon34b  4251  elsn2g  4614  eqoreldif  4635  difsn  4747  elpreqprb  4817  dfnfc2  4878  intmin4  4925  dfiin2g  4979  elpw2g  5269  ssrel  5722  ssrel2  5724  ssrelrel  5735  dmopab2rex  5856  releldmb  5885  relelrnb  5886  cnveqb  6143  dmsnopg  6160  relcnvtrg  6214  elsnxp  6238  onelssex  6355  ord0eln0  6362  f1ocnvb  6776  eqfnun  6970  ffvresb  7058  isof1oopb  7259  soisores  7261  riotaclb  7344  fnoprabg  7469  difex2  7693  dfwe2  7707  ordpwsuc  7745  ordunisuc2  7774  limsssuc  7780  dfom2  7798  relcnvexb  7856  dfsmo2  8267  ord1eln01  8411  ord2eln012  8412  omord  8483  nneob  8571  fsetcdmex  8787  pw2f1olem  8994  pwssfi  9086  sucdom  9128  1sdom  9139  fundmfibi  9220  f1dmvrnfibi  9225  fieq0  9305  hartogslem1  9428  rankr1ag  9695  rankeq0b  9753  fidomtri  9886  fidomtri2  9887  pr2ne  9896  isfin2-2  10210  enfin2i  10212  isfin3-2  10258  isf34lem6  10271  isfin1-2  10276  isfin1-3  10277  isfin7-2  10287  axgroth6  10719  ltsonq  10860  ltexnq  10866  znegclb  12509  rpneg  12924  nltpnft  13063  ngtmnft  13065  xrrebnd  13067  qextlt  13102  qextle  13103  iccneg  13372  fzsn  13466  fz1sbc  13500  fzdif1  13505  fzofzp1b  13665  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  19054  issubg4  19058  eqg0subg  19108  ghmmhmb  19139  pmtrmvd  19368  mndodcong  19454  issubrng2  20473  issubrg2  20507  ring2idlqusb  21247  lpigen  21272  cyggic  21509  ip2eq  21590  maducoeval2  22555  eltg3  22877  bastop  22896  0top  22898  iscld3  22979  isclo2  23003  cnprest  23204  dfconn2  23334  comppfsc  23447  cmphaushmeo  23715  reghaus  23740  nrmhaus  23741  fbun  23755  fsubbas  23782  ufileu  23834  uffix  23836  txflf  23921  fclsrest  23939  flimfnfcls  23943  ptcmplem2  23968  tgpt1  24033  tgpt0  24034  isngp2  24512  nrgdomn  24586  nmhmcn  25047  iscmet3  25220  limcflf  25809  ply1nzb  26055  coe11  26185  dgreq0  26198  eldmgm  26959  sqf11  27076  sqff1o  27119  zabsle1  27234  lgsabs1  27274  lgsquadlem2  27319  madebday  27845  oldbday  27846  slelss  27854  zs12negsclb  28391  issubgr2  29250  uhgrissubgr  29253  usgrfilem  29305  uvtxnbgrb  29379  nbusgrvtxm1uvtx  29383  cusgrfilem3  29436  vdiscusgr  29510  wwlksn0s  29839  clwwlknon1loop  30078  clwwlknun  30092  nmobndi  30755  hmopadj2  31921  mdslle1i  32297  mdslle2i  32298  relfi  32582  ssrelf  32598  prodindf  32844  bnj1173  35014  r1filim  35115  revwlkb  35170  resconn  35290  cvmsval  35310  fmlafvel  35429  dmopab3rexdif  35449  elmrsubrn  35564  funsseq  35812  brcolinear  36103  outsideofeu  36175  lineunray  36191  nn0prpw  36367  bj-nfimexal  36670  bj-sngltag  37027  bj-elpwg  37096  bj-elsn0  37199  bj-opelid  37200  bj-opelidres  37205  bj-ideqg1  37208  bj-imdirval3  37228  bj-inftyexpiinj  37253  wl-ax11-lem2  37630  poimirlem26  37696  poimirlem27  37697  heicant  37705  cover2  37765  isbndx  37832  isbnd2  37833  equivbnd2  37842  prdsbnd2  37845  elghomlem2OLD  37936  isdrngo3  38009  riotaclbgBAD  39063  lssatle  39124  opcon3b  39305  cdlemk33N  41018  cdlemk34  41019  ioin9i8  42310  eu6w  42779  wepwsolem  43145  onsupmaxb  43342  rp-fakeimass  43615  iscard5  43639  cnvssb  43689  intimag  43759  ntrneiiso  44194  pm11.71  44500  pm14.122b  44526  pm14.123b  44529  iotavalb  44533  relwf  45070  elixpconstg  45196  eliuniin  45206  eliuniin2  45227  climreeq  45723  f1cof1b  47187  rexrsb  47210  afv0nbfvbi  47261  dfafn5b  47271  elfz2z  47425  zeo2ALTV  47781  fpprwpprb  47850  dfsclnbgr6  47968  nnlog2ge0lt1  48677  oppccatb  49127