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  359  bimsc1  842  biorf  934  pm4.72  947  19.38a  1835  19.38b  1836  ax13b  2028  19.3t  2190  cgsexg  3509  cgsex2g  3510  cgsex4g  3511  cgsex4gOLD  3512  elab3gf  3671  elab3g  3672  abidnf  3695  reuan  3888  sscon34b  4293  elsn2g  4661  eqoreldif  4683  difsn  4797  elpreqprb  4866  dfnfc2  4929  intmin4  4977  dfiin2g  5032  elpw2g  5341  ssrel  5778  ssrelOLD  5779  ssrel2  5781  ssrelrel  5792  dmopab2rex  5914  releldmb  5942  relelrnb  5943  cnveqb  6197  dmsnopg  6214  relcnvtrg  6267  elsnxp  6292  onelssex  6413  ord0eln0  6420  f1ocnvb  6845  eqfnun  7039  ffvresb  7128  isof1oopb  7326  soisores  7328  riotaclb  7411  fnoprabg  7537  difex2  7757  dfwe2  7771  ordpwsuc  7813  ordunisuc2  7843  limsssuc  7849  dfom2  7867  relcnvexb  7928  dfsmo2  8366  ord1eln01  8515  ord2eln012  8516  omord  8587  nneob  8675  fsetcdmex  8881  pw2f1olem  9103  sucdom  9259  sucdomOLD  9260  1sdom  9272  fundmfibi  9368  f1dmvrnfibi  9373  fieq0  9454  hartogslem1  9575  rankr1ag  9835  rankeq0b  9893  fidomtri  10026  fidomtri2  10027  pr2ne  10037  isfin2-2  10350  enfin2i  10352  isfin3-2  10398  isf34lem6  10411  isfin1-2  10416  isfin1-3  10417  isfin7-2  10427  axgroth6  10859  ltsonq  11000  ltexnq  11006  znegclb  12642  rpneg  13051  nltpnft  13188  ngtmnft  13190  xrrebnd  13192  qextlt  13227  qextle  13228  iccneg  13494  fzsn  13588  fz1sbc  13622  fzofzp1b  13776  ceilidz  13863  fleqceilz  13865  hashclb  14367  hashnncl  14375  hashfun  14446  reim0b  15116  rexanre  15343  rexuzre  15349  lo1resb  15558  o1resb  15560  dvdsext  16315  zob  16353  ncoprmgcdne1b  16643  pceq0  16865  pc11  16874  pcz  16875  ramtcl  17004  cshwsiun  17094  oduposb  18346  pospo  18362  cnvpsb  18596  tsrlemax  18603  issubg2  19128  issubg4  19132  eqg0subg  19183  ghmmhmb  19214  pmtrmvd  19447  mndodcong  19533  issubrng2  20533  issubrg2  20569  ring2idlqusb  21292  lpigen  21317  cyggic  21563  ip2eq  21642  maducoeval2  22627  eltg3  22950  bastop  22969  0top  22971  iscld3  23053  isclo2  23077  cnprest  23278  dfconn2  23408  comppfsc  23521  cmphaushmeo  23789  reghaus  23814  nrmhaus  23815  fbun  23829  fsubbas  23856  ufileu  23908  uffix  23910  txflf  23995  fclsrest  24013  flimfnfcls  24017  ptcmplem2  24042  tgpt1  24107  tgpt0  24108  isngp2  24591  nrgdomn  24673  nmhmcn  25132  iscmet3  25306  limcflf  25895  ply1nzb  26144  coe11  26274  dgreq0  26287  eldmgm  27044  sqf11  27161  sqff1o  27204  zabsle1  27319  lgsabs1  27359  lgsquadlem2  27404  madebday  27917  oldbday  27918  slelss  27925  issubgr2  29202  uhgrissubgr  29205  usgrfilem  29257  uvtxnbgrb  29331  nbusgrvtxm1uvtx  29335  cusgrfilem3  29388  vdiscusgr  29462  wwlksn0s  29789  clwwlknon1loop  30025  clwwlknun  30039  nmobndi  30702  hmopadj2  31868  mdslle1i  32244  mdslle2i  32245  relfi  32519  ssrelf  32532  prodindf  33866  bnj1173  34857  revwlkb  34963  resconn  35084  cvmsval  35104  fmlafvel  35223  dmopab3rexdif  35243  elmrsubrn  35358  funsseq  35601  brcolinear  35893  outsideofeu  35965  lineunray  35981  nn0prpw  36045  bj-nfimexal  36340  bj-sngltag  36700  bj-elpwg  36769  bj-elsn0  36872  bj-opelid  36873  bj-opelidres  36878  bj-ideqg1  36881  bj-imdirval3  36901  bj-inftyexpiinj  36926  wl-ax11-lem2  37291  poimirlem26  37357  poimirlem27  37358  heicant  37366  cover2  37426  isbndx  37493  isbnd2  37494  equivbnd2  37503  prdsbnd2  37506  elghomlem2OLD  37597  isdrngo3  37670  riotaclbgBAD  38662  lssatle  38723  opcon3b  38904  cdlemk33N  40618  cdlemk34  40619  ioin9i8  41949  eu6w  42366  wepwsolem  42737  onsupmaxb  42938  rp-fakeimass  43213  iscard5  43237  cnvssb  43287  intimag  43357  ntrneiiso  43792  pm11.71  44105  pm14.122b  44131  pm14.123b  44134  iotavalb  44138  elixpconstg  44724  eliuniin  44734  eliuniin2  44755  climreeq  45267  f1cof1b  46723  rexrsb  46746  afv0nbfvbi  46797  dfafn5b  46807  elfz2z  46961  zeo2ALTV  47276  fpprwpprb  47345  dfsclnbgr6  47458  nnlog2ge0lt1  47987