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  360  bimsc1  842  biorf  935  pm4.72  948  19.38a  1842  19.38b  1843  ax13b  2035  19.3t  2194  cgsexg  3518  cgsex2g  3519  cgsex4g  3520  cgsex4gOLD  3521  cgsex4gOLDOLD  3522  elab3gf  3673  elab3g  3674  abidnf  3697  reuan  3889  sscon34b  4293  elsn2g  4665  eqoreldif  4687  difsn  4800  elpreqprb  4867  dfnfc2  4932  intmin4  4980  dfiin2g  5034  elpw2g  5343  ssrel  5780  ssrelOLD  5781  ssrel2  5783  ssrelrel  5794  dmopab2rex  5915  releldmb  5943  relelrnb  5944  cnveqb  6192  dmsnopg  6209  relcnvtrg  6262  elsnxp  6287  onelssex  6409  ord0eln0  6416  f1ocnvb  6843  eqfnun  7035  ffvresb  7120  isof1oopb  7318  soisores  7320  riotaclb  7403  fnoprabg  7527  difex2  7743  dfwe2  7757  ordpwsuc  7799  ordunisuc2  7829  limsssuc  7835  dfom2  7853  relcnvexb  7913  dfsmo2  8343  ord1eln01  8492  ord2eln012  8493  omord  8564  nneob  8651  fsetcdmex  8853  pw2f1olem  9072  sucdom  9231  sucdomOLD  9232  1sdom  9244  fundmfibi  9327  f1dmvrnfibi  9332  fieq0  9412  hartogslem1  9533  rankr1ag  9793  rankeq0b  9851  fidomtri  9984  fidomtri2  9985  pr2ne  9995  isfin2-2  10310  enfin2i  10312  isfin3-2  10358  isf34lem6  10371  isfin1-2  10376  isfin1-3  10377  isfin7-2  10387  axgroth6  10819  ltsonq  10960  ltexnq  10966  znegclb  12595  rpneg  13002  nltpnft  13139  ngtmnft  13141  xrrebnd  13143  qextlt  13178  qextle  13179  iccneg  13445  fzsn  13539  fz1sbc  13573  fzofzp1b  13726  ceilidz  13813  fleqceilz  13815  hashclb  14314  hashnncl  14322  hashfun  14393  reim0b  15062  rexanre  15289  rexuzre  15295  lo1resb  15504  o1resb  15506  dvdsext  16260  zob  16298  ncoprmgcdne1b  16583  pceq0  16800  pc11  16809  pcz  16810  ramtcl  16939  cshwsiun  17029  oduposb  18278  pospo  18294  cnvpsb  18528  tsrlemax  18535  issubg2  19015  issubg4  19019  eqg0subg  19067  ghmmhmb  19097  pmtrmvd  19318  mndodcong  19404  issubrg2  20375  lpigen  20886  cyggic  21119  ip2eq  21197  maducoeval2  22133  eltg3  22456  bastop  22475  0top  22477  iscld3  22559  isclo2  22583  cnprest  22784  dfconn2  22914  comppfsc  23027  cmphaushmeo  23295  reghaus  23320  nrmhaus  23321  fbun  23335  fsubbas  23362  ufileu  23414  uffix  23416  txflf  23501  fclsrest  23519  flimfnfcls  23523  ptcmplem2  23548  tgpt1  23613  tgpt0  23614  isngp2  24097  nrgdomn  24179  nmhmcn  24627  iscmet3  24801  limcflf  25389  ply1nzb  25631  coe11  25758  dgreq0  25770  eldmgm  26515  sqf11  26632  sqff1o  26675  zabsle1  26788  lgsabs1  26828  lgsquadlem2  26873  madebday  27383  oldbday  27384  issubgr2  28518  uhgrissubgr  28521  usgrfilem  28573  uvtxnbgrb  28647  nbusgrvtxm1uvtx  28651  cusgrfilem3  28703  vdiscusgr  28777  wwlksn0s  29104  clwwlknon1loop  29340  clwwlknun  29354  nmobndi  30015  hmopadj2  31181  mdslle1i  31557  mdslle2i  31558  relfi  31820  ssrelf  31831  prodindf  33009  bnj1173  34001  revwlkb  34104  resconn  34225  cvmsval  34245  fmlafvel  34364  dmopab3rexdif  34384  elmrsubrn  34499  funsseq  34727  brcolinear  35019  outsideofeu  35091  lineunray  35107  nn0prpw  35196  bj-nfimexal  35491  bj-sngltag  35852  bj-elpwg  35921  bj-elsn0  36024  bj-opelid  36025  bj-opelidres  36030  bj-ideqg1  36033  bj-imdirval3  36053  bj-inftyexpiinj  36078  wl-ax11-lem2  36436  poimirlem26  36502  poimirlem27  36503  heicant  36511  cover2  36571  isbndx  36638  isbnd2  36639  equivbnd2  36648  prdsbnd2  36651  elghomlem2OLD  36742  isdrngo3  36815  riotaclbgBAD  37812  lssatle  37873  opcon3b  38054  cdlemk33N  39768  cdlemk34  39769  ioin9i8  41019  wepwsolem  41769  onsupmaxb  41973  rp-fakeimass  42248  iscard5  42272  cnvssb  42322  intimag  42392  ntrneiiso  42827  pm11.71  43141  pm14.122b  43167  pm14.123b  43170  iotavalb  43174  elixpconstg  43763  eliuniin  43773  eliuniin2  43794  climreeq  44315  f1cof1b  45771  rexrsb  45794  afv0nbfvbi  45845  dfafn5b  45855  elfz2z  46009  zeo2ALTV  46325  fpprwpprb  46394  issubrng2  46721  ring2idlqusb  46775  nnlog2ge0lt1  47205