Theorem impbid2 225

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimt  361  bimsc1  843  biorf  936  pm4.72  949  19.38a  1843  19.38b  1844  ax13b  2036  19.3t  2195  cgsexg  3519  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  elab3gf  3675  elab3g  3676  abidnf  3699  reuan  3891  sscon34b  4295  elsn2g  4667  eqoreldif  4689  difsn  4802  elpreqprb  4869  dfnfc2  4934  intmin4  4982  dfiin2g  5036  elpw2g  5345  ssrel  5783  ssrelOLD  5784  ssrel2  5786  ssrelrel  5797  dmopab2rex  5918  releldmb  5946  relelrnb  5947  cnveqb  6196  dmsnopg  6213  relcnvtrg  6266  elsnxp  6291  onelssex  6413  ord0eln0  6420  f1ocnvb  6847  eqfnun  7039  ffvresb  7124  isof1oopb  7322  soisores  7324  riotaclb  7407  fnoprabg  7531  difex2  7747  dfwe2  7761  ordpwsuc  7803  ordunisuc2  7833  limsssuc  7839  dfom2  7857  relcnvexb  7917  dfsmo2  8347  ord1eln01  8496  ord2eln012  8497  omord  8568  nneob  8655  fsetcdmex  8857  pw2f1olem  9076  sucdom  9235  sucdomOLD  9236  1sdom  9248  fundmfibi  9331  f1dmvrnfibi  9336  fieq0  9416  hartogslem1  9537  rankr1ag  9797  rankeq0b  9855  fidomtri  9988  fidomtri2  9989  pr2ne  9999  isfin2-2  10314  enfin2i  10316  isfin3-2  10362  isf34lem6  10375  isfin1-2  10380  isfin1-3  10381  isfin7-2  10391  axgroth6  10823  ltsonq  10964  ltexnq  10970  znegclb  12599  rpneg  13006  nltpnft  13143  ngtmnft  13145  xrrebnd  13147  qextlt  13182  qextle  13183  iccneg  13449  fzsn  13543  fz1sbc  13577  fzofzp1b  13730  ceilidz  13817  fleqceilz  13819  hashclb  14318  hashnncl  14326  hashfun  14397  reim0b  15066  rexanre  15293  rexuzre  15299  lo1resb  15508  o1resb  15510  dvdsext  16264  zob  16302  ncoprmgcdne1b  16587  pceq0  16804  pc11  16813  pcz  16814  ramtcl  16943  cshwsiun  17033  oduposb  18282  pospo  18298  cnvpsb  18532  tsrlemax  18539  issubg2  19021  issubg4  19025  eqg0subg  19073  ghmmhmb  19103  pmtrmvd  19324  mndodcong  19410  issubrg2  20339  lpigen  20894  cyggic  21128  ip2eq  21206  maducoeval2  22142  eltg3  22465  bastop  22484  0top  22486  iscld3  22568  isclo2  22592  cnprest  22793  dfconn2  22923  comppfsc  23036  cmphaushmeo  23304  reghaus  23329  nrmhaus  23330  fbun  23344  fsubbas  23371  ufileu  23423  uffix  23425  txflf  23510  fclsrest  23528  flimfnfcls  23532  ptcmplem2  23557  tgpt1  23622  tgpt0  23623  isngp2  24106  nrgdomn  24188  nmhmcn  24636  iscmet3  24810  limcflf  25398  ply1nzb  25640  coe11  25767  dgreq0  25779  eldmgm  26526  sqf11  26643  sqff1o  26686  zabsle1  26799  lgsabs1  26839  lgsquadlem2  26884  madebday  27394  oldbday  27395  issubgr2  28529  uhgrissubgr  28532  usgrfilem  28584  uvtxnbgrb  28658  nbusgrvtxm1uvtx  28662  cusgrfilem3  28714  vdiscusgr  28788  wwlksn0s  29115  clwwlknon1loop  29351  clwwlknun  29365  nmobndi  30028  hmopadj2  31194  mdslle1i  31570  mdslle2i  31571  relfi  31833  ssrelf  31844  prodindf  33021  bnj1173  34013  revwlkb  34116  resconn  34237  cvmsval  34257  fmlafvel  34376  dmopab3rexdif  34396  elmrsubrn  34511  funsseq  34739  brcolinear  35031  outsideofeu  35103  lineunray  35119  nn0prpw  35208  bj-nfimexal  35503  bj-sngltag  35864  bj-elpwg  35933  bj-elsn0  36036  bj-opelid  36037  bj-opelidres  36042  bj-ideqg1  36045  bj-imdirval3  36065  bj-inftyexpiinj  36090  wl-ax11-lem2  36448  poimirlem26  36514  poimirlem27  36515  heicant  36523  cover2  36583  isbndx  36650  isbnd2  36651  equivbnd2  36660  prdsbnd2  36663  elghomlem2OLD  36754  isdrngo3  36827  riotaclbgBAD  37824  lssatle  37885  opcon3b  38066  cdlemk33N  39780  cdlemk34  39781  ioin9i8  41024  wepwsolem  41784  onsupmaxb  41988  rp-fakeimass  42263  iscard5  42287  cnvssb  42337  intimag  42407  ntrneiiso  42842  pm11.71  43156  pm14.122b  43182  pm14.123b  43185  iotavalb  43189  elixpconstg  43778  eliuniin  43788  eliuniin2  43809  climreeq  44329  f1cof1b  45785  rexrsb  45808  afv0nbfvbi  45859  dfafn5b  45869  elfz2z  46023  zeo2ALTV  46339  fpprwpprb  46408  issubrng2  46737  ring2idlqusb  46795  nnlog2ge0lt1  47252