Theorem impbid2 215

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  biimt  349  biorf  419  biorfiOLD  422  pm4.72  916  biort  936  bimsc1  976  ax13b  1951  cgsexg  3211  cgsex2g  3212  cgsex4g  3213  elab3gf  3325  abidnf  3342  elsn2g  4157  eqoreldif  4172  difsn  4269  eqsnOLD  4302  prel12  4323  elpreqprb  4335  dfnfc2  4390  dfnfc2OLD  4391  intmin4  4441  dfiin2g  4489  elpw2g  4754  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  releldmb  5281  relelrnb  5282  cnveqb  5508  dmsnopg  5524  relcnvtr  5572  elsnxp  5594  ord0eln0  5696  f1ocnvb  6063  ffvresb  6301  isof1oopb  6475  soisores  6477  riotaclb  6548  fnoprabg  6659  difex2  6863  dfwe2  6873  ordpwsuc  6907  ordunisuc2  6936  limsssuc  6942  dfom2  6959  relcnvexb  7007  dfsmo2  7331  omord  7535  nneob  7619  pw2f1olem  7949  sucdom  8042  fundmfibi  8130  f1dmvrnfibi  8133  fieq0  8210  hartogslem1  8330  rankr1ag  8548  rankeq0b  8606  fidomtri  8702  fidomtri2  8703  isfin2-2  9024  enfin2i  9026  isfin3-2  9072  isf34lem6  9085  isfin1-2  9090  isfin1-3  9091  isfin7-2  9101  axgroth6  9529  ltsonq  9670  ltexnq  9676  znegclb  11291  rpneg  11739  nltpnft  11871  ngtmnft  11872  xrrebnd  11873  qextlt  11908  qextle  11909  iccneg  12164  fzsn  12254  fz1sbc  12285  fzofzp1b  12432  ceilidz  12513  fleqceilz  12515  hashclb  13011  hashnncl  13018  hashfun  13084  reim0b  13707  rexanre  13934  rexuzre  13940  lo1resb  14143  o1resb  14145  dvdsext  14881  zob  14921  ncoprmgcdne1b  15201  pceq0  15413  pc11  15422  pcz  15423  ramtcl  15552  cshwsiun  15644  pospo  16796  oduposb  16959  cnvpsb  17036  tsrlemax  17043  issubg2  17432  issubg4  17436  ghmmhmb  17494  pmtrmvd  17699  mndodcong  17784  issubrg2  18623  lpigen  19077  cyggic  19740  ip2eq  19817  maducoeval2  20265  eltg3  20577  bastop  20596  0top  20598  iscld3  20678  isclo2  20702  cnprest  20903  dfcon2  21032  comppfsc  21145  cmphaushmeo  21413  reghaus  21438  nrmhaus  21439  fbun  21454  fsubbas  21481  ufileu  21533  uffix  21535  txflf  21620  fclsrest  21638  flimfnfcls  21642  ptcmplem2  21667  tgpt1  21731  tgpt0  21732  isngp2  22211  nrgdomn  22285  nmhmcn  22728  iscmet3  22899  limcflf  23451  ply1nzb  23686  coe11  23813  dgreq0  23825  eldmgm  24548  sqf11  24665  sqff1o  24708  zabsle1  24821  lgsabs1  24861  lgsquadlem2  24906  usgrafilem2  25941  cusgrafilem3  26009  iswlkg  26052  wwlkn0s  26233  isclwlkg  26283  el2wlksoton  26405  el2spthsoton  26406  vdiscusgra  26448  nmobndi  27014  hmopadj2  28184  mdslle1i  28560  mdslle2i  28561  relfi  28797  ssrelf  28805  bnj1173  30324  rescon  30482  cvmsval  30502  elmrsubrn  30671  funsseq  30912  brcolinear  31336  outsideofeu  31408  lineunray  31424  nn0prpw  31488  bj-19.3t  31876  bj-sb3b  31992  bj-sngltag  32164  bj-elid2  32263  bj-inftyexpiinj  32273  wl-sb5nae  32519  wl-ax11-lem2  32542  poimirlem26  32605  poimirlem27  32606  heicant  32614  cover2  32678  eqfnun  32686  isbndx  32751  isbnd2  32752  equivbnd2  32761  prdsbnd2  32764  elghomlem2OLD  32855  isdrngo3  32928  riotaclbgBAD  33258  lssatle  33320  opcon3b  33501  cdlemk33N  35215  cdlemk34  35216  wepwsolem  36630  rp-fakeimass  36876  cnvssb  36911  intimag  36967  sscon34b  37337  ntrneiiso  37409  pm11.71  37619  pm14.122b  37646  pm14.123b  37649  iotavalb  37653  climreeq  38680  rexrsb  39818  reuan  39829  afv0nbfvbi  39880  dfafn5b  39890  zeo2ALTV  40120  elfz2z  40352  issubgr2  40496  uhgrissubgr  40499  usgrfilem  40546  uvtxnbgrb  40628  cusgrfilem3  40673  vdiscusgr  40747  wwlksn0s  41057  nnlog2ge0lt1  42158