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  2031  19.3t  2201  cgsexg  3505  cgsex2g  3506  cgsex4g  3507  cgsex4gOLD  3508  elab3gf  3663  elab3g  3664  abidnf  3685  reuan  3871  sscon34b  4279  elsn2g  4640  eqoreldif  4661  difsn  4774  elpreqprb  4844  dfnfc2  4905  intmin4  4953  dfiin2g  5008  elpw2g  5303  ssrel  5761  ssrelOLD  5762  ssrel2  5764  ssrelrel  5775  dmopab2rex  5897  releldmb  5926  relelrnb  5927  cnveqb  6185  dmsnopg  6202  relcnvtrg  6255  elsnxp  6280  onelssex  6401  ord0eln0  6408  f1ocnvb  6831  eqfnun  7027  ffvresb  7115  isof1oopb  7318  soisores  7320  riotaclb  7403  fnoprabg  7530  difex2  7754  dfwe2  7768  ordpwsuc  7809  ordunisuc2  7839  limsssuc  7845  dfom2  7863  relcnvexb  7922  dfsmo2  8361  ord1eln01  8508  ord2eln012  8509  omord  8580  nneob  8668  fsetcdmex  8877  pw2f1olem  9090  pwssfi  9191  sucdom  9243  sucdomOLD  9244  1sdom  9256  fundmfibi  9348  f1dmvrnfibi  9353  fieq0  9433  hartogslem1  9556  rankr1ag  9816  rankeq0b  9874  fidomtri  10007  fidomtri2  10008  pr2ne  10018  isfin2-2  10333  enfin2i  10335  isfin3-2  10381  isf34lem6  10394  isfin1-2  10399  isfin1-3  10400  isfin7-2  10410  axgroth6  10842  ltsonq  10983  ltexnq  10989  znegclb  12629  rpneg  13041  nltpnft  13180  ngtmnft  13182  xrrebnd  13184  qextlt  13219  qextle  13220  iccneg  13489  fzsn  13583  fz1sbc  13617  fzdif1  13622  fzofzp1b  13781  ceilidz  13869  fleqceilz  13871  hashclb  14376  hashnncl  14384  hashfun  14455  reim0b  15138  rexanre  15365  rexuzre  15371  lo1resb  15580  o1resb  15582  dvdsext  16340  zob  16378  ncoprmgcdne1b  16669  pceq0  16891  pc11  16900  pcz  16901  ramtcl  17030  cshwsiun  17119  oduposb  18339  pospo  18355  cnvpsb  18589  tsrlemax  18596  issubg2  19124  issubg4  19128  eqg0subg  19179  ghmmhmb  19210  pmtrmvd  19437  mndodcong  19523  issubrng2  20518  issubrg2  20552  ring2idlqusb  21271  lpigen  21296  cyggic  21533  ip2eq  21613  maducoeval2  22578  eltg3  22900  bastop  22919  0top  22921  iscld3  23002  isclo2  23026  cnprest  23227  dfconn2  23357  comppfsc  23470  cmphaushmeo  23738  reghaus  23763  nrmhaus  23764  fbun  23778  fsubbas  23805  ufileu  23857  uffix  23859  txflf  23944  fclsrest  23962  flimfnfcls  23966  ptcmplem2  23991  tgpt1  24056  tgpt0  24057  isngp2  24536  nrgdomn  24610  nmhmcn  25071  iscmet3  25245  limcflf  25834  ply1nzb  26080  coe11  26210  dgreq0  26223  eldmgm  26984  sqf11  27101  sqff1o  27144  zabsle1  27259  lgsabs1  27299  lgsquadlem2  27344  madebday  27863  oldbday  27864  slelss  27872  zs12negsclb  28393  issubgr2  29251  uhgrissubgr  29254  usgrfilem  29306  uvtxnbgrb  29380  nbusgrvtxm1uvtx  29384  cusgrfilem3  29437  vdiscusgr  29511  wwlksn0s  29843  clwwlknon1loop  30079  clwwlknun  30093  nmobndi  30756  hmopadj2  31922  mdslle1i  32298  mdslle2i  32299  relfi  32583  ssrelf  32595  prodindf  32840  bnj1173  35033  revwlkb  35148  resconn  35268  cvmsval  35288  fmlafvel  35407  dmopab3rexdif  35427  elmrsubrn  35542  funsseq  35785  brcolinear  36077  outsideofeu  36149  lineunray  36165  nn0prpw  36341  bj-nfimexal  36644  bj-sngltag  37001  bj-elpwg  37070  bj-elsn0  37173  bj-opelid  37174  bj-opelidres  37179  bj-ideqg1  37182  bj-imdirval3  37202  bj-inftyexpiinj  37227  wl-ax11-lem2  37604  poimirlem26  37670  poimirlem27  37671  heicant  37679  cover2  37739  isbndx  37806  isbnd2  37807  equivbnd2  37816  prdsbnd2  37819  elghomlem2OLD  37910  isdrngo3  37983  riotaclbgBAD  38972  lssatle  39033  opcon3b  39214  cdlemk33N  40928  cdlemk34  40929  ioin9i8  42258  eu6w  42699  wepwsolem  43066  onsupmaxb  43263  rp-fakeimass  43536  iscard5  43560  cnvssb  43610  intimag  43680  ntrneiiso  44115  pm11.71  44421  pm14.122b  44447  pm14.123b  44450  iotavalb  44454  relwf  44992  elixpconstg  45113  eliuniin  45123  eliuniin2  45144  climreeq  45642  f1cof1b  47106  rexrsb  47129  afv0nbfvbi  47180  dfafn5b  47190  elfz2z  47344  zeo2ALTV  47685  fpprwpprb  47754  dfsclnbgr6  47871  nnlog2ge0lt1  48546  oppccatb  48991